diff --git a/src/acg-data/signature.ml b/src/acg-data/signature.ml
index c58215c23077f9c9fe167f8d31b0ff77c706407c..f63aff8dff9d034e4be937985bb5d5e859513178 100644
--- a/src/acg-data/signature.ml
+++ b/src/acg-data/signature.ml
@@ -387,26 +387,29 @@ struct
 	      with 
 		| Not_functional_type -> let u_loc = get_location u in
 		    raise (Error.Error (Error.Type_error (Error.Is_Used (Lambda.type_to_string u_type (id_to_string sg),"\"'a -> 'b\" or \"'a => 'b\" in order to enable application"),(fst u_loc,snd u_loc)))) in
-	      try
-		let v_term,_,new_new_typing_env = 
-		  match lin with
-		    | Abstract_syntax.Linear -> typecheck_aux v (Some (local_expand ty1)) new_typing_env
-		    | Abstract_syntax.Non_linear ->
-			let non_lin_env = remove_lin_context new_typing_env in
-(*			let () = Printf.printf "Inserting wrapper\n%!" in *)
-			let v_t,v_ty,{wrapper=w} = typecheck_aux v (Some (local_expand ty1)) {non_lin_env with wrapper=Some (get_location u,u_type,get_location v)} in
-			  v_t,v_ty,{new_typing_env with wrapper=w} in
-		  match ty with
-		    | None -> Lambda.App (u_term,v_term),ty2,new_new_typing_env
-		    | Some l_ty when l_ty=local_expand ty2 -> Lambda.App (u_term,v_term),l_ty,new_new_typing_env
-		    | Some l_ty -> raise (Type_mismatch (l,l_ty,ty2)) 
-	      with
-		| Non_empty_linear_context (x,l) ->
-		    let func_loc,func_st,v_loc = match tenv.wrapper with
-		      | None -> failwith "Bug"
-		      | Some a  ->a in
-(*		    let v_loc = get_location v in*)
-		      raise (Error.Error (Error.Type_error (Error.Non_empty_context (x,l,func_loc,Lambda.type_to_string func_st (id_to_string sg)),v_loc))) in 
+	    let v_term,_,new_new_typing_env = 
+	      match lin with
+		| Abstract_syntax.Linear -> typecheck_aux v (Some (local_expand ty1)) new_typing_env
+		| Abstract_syntax.Non_linear ->
+		    let non_lin_env = remove_lin_context new_typing_env in
+		      (*			let () = Printf.printf "Inserting wrapper\n%!" in *)
+		    let wrapper = get_location u,u_type,get_location v in
+		      try
+			let v_t,v_ty,{wrapper=w} =
+			  typecheck_aux v (Some (local_expand ty1)) {non_lin_env with wrapper=Some wrapper} in
+			  v_t,v_ty,{new_typing_env with wrapper=w} 
+		      with
+			| Non_empty_linear_context (x,l) ->
+			    let func_loc,func_st,v_loc = match tenv.wrapper with
+			      | None -> wrapper
+			      | Some a  -> a in
+			      (*		    let v_loc = get_location v in*)
+			      raise (Error.Error (Error.Type_error (Error.Non_empty_context (x,l,func_loc,Lambda.type_to_string func_st (id_to_string sg)),v_loc)))
+	    in
+	      match ty with
+		| None -> Lambda.App (u_term,v_term),ty2,new_new_typing_env
+		| Some l_ty when l_ty=local_expand ty2 -> Lambda.App (u_term,v_term),l_ty,new_new_typing_env
+		| Some l_ty -> raise (Type_mismatch (l,l_ty,ty2))  in 
       try
 	let t_term,t_type,(_:typing_environment) = 
 	  typecheck_aux t (Some (local_expand ty)) {linear_level=0;level=0;env=Utils.StringMap.empty;wrapper=None} in    
diff --git a/src/data/drt4.acg b/src/data/drt4.acg
index 68cf08ec815b5b828ab0752ca68c00072678783a..6ccdacf17c0146b3e33de51f6e227b2e57c898d5 100644
--- a/src/data/drt4.acg
+++ b/src/data/drt4.acg
@@ -60,7 +60,7 @@ signature semantics =
 	o = g => g => ( g => g => t =>t ) => t:type ;
 
 	vt = Lambda v O S.S(Lambda x.O(Lambda y.Lambda e1 e2 phi. phi e1 e2 (v x y))) : (e => e => t) => ((e =>o ) => o)  => ((e =>o ) => o) => o ;
-	n = Lambda n .Lambda x.Lambda c e1 e2.Lambda phi. phi e1 e2 (n x)  : (e => t) => e => o;
+	n = Lambda n .Lambda x.Lambda c e1 e2. Lambda phi. phi  e1 e2 (n x)  : (e => t) => e => o;
 end
 
 lexicon drt (syntax):semantics =