diff --git a/src/parser/typing.ml b/src/parser/typing.ml
index 90fffc38ddea0f297e8c5f83990cb36d983f0645..d45a0f90b34e6e88356912733f90a74b61e53381 100644
--- a/src/parser/typing.ml
+++ b/src/parser/typing.ml
@@ -298,31 +298,23 @@ let find_lsymbol_ns p ns =
 let find_lsymbol p th = 
   find_lsymbol_ns p (get_namespace th)
 
-let specialize_fsymbol ~loc s =
-  let tl, t = match s.ls_value with
-    | Some t -> s.ls_args, t
-    | _ -> assert false (* FIXME: is it right? *)
-  in
+let specialize_lsymbol ~loc s =
+  let tl = s.ls_args in
+  let t = s.ls_value in
   let env = Htv.create 17 in
-  s, List.map (specialize ~loc env) tl, specialize ?loc env t
-
-let find_lsymbol {id=x; id_loc=loc} ns = 
-  try Mnm.find x ns.ns_ls
-  with Not_found -> error ~loc (UnboundSymbol x)
-
-let find_lsymbol_ns p ns =
-  find find_lsymbol p ns
+  s, List.map (specialize ~loc env) tl, option_map (specialize ~loc env) t
 
-let find_lsymbol p th =
-  find_lsymbol_ns p (get_namespace th)
+let specialize_fsymbol ~loc s = 
+  let s, tl, ty = specialize_lsymbol ~loc s in
+  match ty with
+    | None -> error ~loc TermExpected
+    | Some ty -> s, tl, ty
 
-let specialize_psymbol ~loc s =
-  let tl = match s.ls_value with
-    | None -> s.ls_args
-    | _ -> assert false (* FIXME: is it right? *)
-  in
-  let env = Htv.create 17 in
-  s, List.map (specialize ~loc env) tl
+let specialize_psymbol ~loc s = 
+  let s, tl, ty = specialize_lsymbol ~loc s in
+  match ty with
+    | None -> s, tl
+    | Some _ -> error ~loc PredicateExpected
 
 (** Typing types *)
 
@@ -461,6 +453,14 @@ let rec trigger_not_a_term_exn = function
   | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
   | _ -> false
 
+let check_linearity uqu =
+  let s = ref S.empty in
+  let check id = 
+    if S.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
+    s := S.add id.id !s
+  in
+  List.iter (fun (idl, _) -> List.iter check idl) uqu
+
 let rec dterm env t = 
   let n, ty = dterm_node t.pp_loc env t.pp_desc in
   { dt_node = n; dt_ty = ty }
@@ -521,6 +521,7 @@ and dfmla env e = match e.pp_desc with
   | PPif (a, b, c) ->
       Fif (dfmla env a, dfmla env b, dfmla env c)  
   | PPquant (q, uqu, trl, a) ->
+      check_linearity uqu;
       let uquant env (idl,ty) =
         let ty = dty env ty in
         let env, idl = 
diff --git a/src/test.why b/src/test.why
index a0e4635ee85b69d5257860c8a9554adfa6aaa8d4..67a6949db96eb992df4266472a287c7a80db3453 100644
--- a/src/test.why
+++ b/src/test.why
@@ -3,8 +3,8 @@
 
 theory A
   use import prelude.Int
-  axiom A : 
-    F : let x = 2+2 in G : x*x = 16
+  logic p(int, int)
+  axiom A : forall x,y:int, z,t:real. x=x
 end
 
 theory TreeForest
diff --git a/src/util/util.ml b/src/util/util.ml
index f04dd2ed0e512aba131437075a80807cb8588328..5c36e58abaa1764225c17ae726bcd595ea8f796f 100644
--- a/src/util/util.ml
+++ b/src/util/util.ml
@@ -24,6 +24,8 @@ let map_fold_left f acc l =
 
 let of_option = function Some v -> v | None -> assert false
 
+let option_map f = function None -> None | Some x -> Some (f x)
+
 exception FoldSkip
 
 let all_fn pr _ t = pr t || raise FoldSkip
diff --git a/src/util/util.mli b/src/util/util.mli
index 6edecbd801b07d2bd7c40c397a84d160975f786a..0d4883016c47d73f799111e29f578d2ce476e248 100644
--- a/src/util/util.mli
+++ b/src/util/util.mli
@@ -19,6 +19,8 @@ val map_fold_left :
 
 val of_option : 'a option -> 'a
 
+val option_map : ('a -> 'b) -> 'a option -> 'b option
+
 exception FoldSkip
 
 val all_fn : ('a -> bool) -> 'b -> 'a -> bool