src/Pure/type.ML

 
 (*Instantiation of type variables in terms *)
 fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
 
 
-(* expand_typ *)
-
-fun expand_typ (TySg {abbrs, ...}) ty =
+(* norm_typ *)
+
+fun norm_typ (TySg {abbrs, ...}) ty =
   let
     val idx = maxidx_of_typ ty + 1;
 
     fun expand (Type (a, Ts)) =
           (case assoc (abbrs, a) of

           | None => Type (a, map expand Ts))
       | expand T = T
   in
     expand ty
   end;
-
-val norm_typ = expand_typ;
-
 
 
 (** type matching **)
 
 exception TYPE_MATCH;