src/Pure/sign.ML
changeset 2144 ddb8499c772b
parent 2138 056dead45ae8
child 2180 934572a94139
equal deleted inserted replaced
2143:093bbe6d333b 2144:ddb8499c772b
   220 
   220 
   221 fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   221 fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   222 
   222 
   223 (* check for duplicate TVars with distinct sorts *)
   223 (* check for duplicate TVars with distinct sorts *)
   224 fun nodup_TVars(tvars,T) = (case T of
   224 fun nodup_TVars(tvars,T) = (case T of
   225       Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
   225       Type(_,Ts) => nodup_TVars_list (tvars,Ts)
   226     | TFree _ => tvars
   226     | TFree _ => tvars
   227     | TVar(v as (a,S)) =>
   227     | TVar(v as (a,S)) =>
   228         (case assoc_string_int(tvars,a) of
   228         (case assoc_string_int(tvars,a) of
   229            Some(S') => if S=S' then tvars
   229            Some(S') => if S=S' then tvars
   230                        else raise_type
   230                        else raise_type
   231                             ("Type variable "^Syntax.string_of_vname a^
   231                             ("Type variable "^Syntax.string_of_vname a^
   232                              " has two distinct sorts") [TVar(a,S'),T] []
   232                              " has two distinct sorts") [TVar(a,S'),T] []
   233          | None => v::tvars));
   233          | None => v::tvars))
       
   234 and (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
       
   235     nodup_TVars_list (tvars,[]) = tvars
       
   236   | nodup_TVars_list (tvars,T::Ts) = nodup_TVars_list(nodup_TVars(tvars,T), 
       
   237 						      Ts);
   234 
   238 
   235 (* check for duplicate Vars with distinct types *)
   239 (* check for duplicate Vars with distinct types *)
   236 fun nodup_Vars tm =
   240 fun nodup_Vars tm =
   237 let fun nodups vars tvars tm = (case tm of
   241 let fun nodups vars tvars tm = (case tm of
   238           Const(c,T) => (vars, nodup_TVars(tvars,T))
   242           Const(c,T) => (vars, nodup_TVars(tvars,T))