src/Pure/sign.ML

     val same_sg: sg * sg -> bool
     val is_draft: sg -> bool
     val const_type: sg -> string -> typ option
     val classes: sg -> class list
     val subsort: sg -> sort * sort -> bool
+    val nodup_Vars: term -> unit
     val norm_sort: sg -> sort -> sort
     val nonempty_sort: sg -> sort list -> sort -> bool
     val print_sg: sg -> unit
     val pretty_sg: sg -> Pretty.T
     val pprint_sg: sg -> pprint_args -> unit

 
 (** certify types and terms **)   (*exception TYPE*)
 
 fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
 
+(* check for duplicate TVars with distinct sorts *)
+fun nodup_TVars(tvars,T) = (case T of
+      Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
+    | TFree _ => tvars
+    | TVar(v as (a,S)) =>
+        (case assoc(tvars,a) of
+           Some(S') => if S=S' then tvars
+                       else raise_type
+                            ("Type variable "^Syntax.string_of_vname a^
+                             "has two distinct sorts") [TVar(a,S'),T] []
+         | None => v::tvars));
+
+(* check for duplicate Vars with distinct types *)
+fun nodup_Vars tm =
+let fun nodups vars tvars tm = (case tm of
+          Const(c,T) => (vars, nodup_TVars(tvars,T))
+        | Free(a,T) => (vars, nodup_TVars(tvars,T))
+        | Var(v as (ixn,T)) =>
+            (case assoc(vars,ixn) of
+               Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
+                           else raise_type
+                             ("Variable "^Syntax.string_of_vname ixn^
+                              "has two distinct types") [T',T] []
+             | None => (v::vars,tvars))
+        | Bound _ => (vars,tvars)
+        | Abs(_,T,t) => nodups vars (nodup_TVars(tvars,T)) t
+        | s$t => let val (vars',tvars') = nodups vars tvars s
+                 in nodups vars' tvars' t end);
+in nodups [] [] tm; () end;
 
 fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
   | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
   | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
 

 
     val norm_tm =
       (case it_term_types (typ_errors tsig) (tm, []) of
         [] => map_term_types (norm_typ tsig) tm
       | errs => raise_type (cat_lines errs) [] [tm]);
+    val _ = nodup_Vars norm_tm;
   in
     (case mapfilt_atoms atom_err norm_tm of
       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
     | errs => raise_type (cat_lines errs) [] [norm_tm])
   end;