# HG changeset patch
# User clasohm
# Date 823864682 -3600
# Node ID b43cd8a8061f0415f7aee526fccc32ec3d2ca247
# Parent  617ca7312ceb3e17757cbe39b6b6fcdd507978a9
renamed expand_typ to norm_typ

diff -r 617ca7312ceb -r b43cd8a8061f src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Feb 08 12:26:16 1996 +0100
+++ b/src/Pure/type.ML	Fri Feb 09 12:18:02 1996 +0100
@@ -333,9 +333,9 @@
 fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye));
 
 
-(* expand_typ *)
+(* norm_typ *)
 
-fun expand_typ (TySg {abbrs, ...}) ty =
+fun norm_typ (TySg {abbrs, ...}) ty =
   let
     val idx = maxidx_of_typ ty + 1;
 
@@ -349,9 +349,6 @@
     expand ty
   end;
 
-val norm_typ = expand_typ;
-
-
 
 (** type matching **)