# HG changeset patch
# User berghofe
# Date 1034333272 -7200
# Node ID 430310b12c5b14fa27f9fc5a5d1bfbcd7359721a
# Parent  7e09ff716dc90b801d65698e148326af89b59d15
norm_typ -> Envir.norm_type

diff -r 7e09ff716dc9 -r 430310b12c5b src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Oct 10 19:24:34 2002 +0200
+++ b/src/Pure/pattern.ML	Fri Oct 11 12:47:52 2002 +0200
@@ -61,17 +61,10 @@
 fun bname binders i = fst(nth_elem(i,binders));
 fun bnames binders is = space_implode " " (map (bname binders) is);
 
-fun norm_typ tye =
-  let fun chase(v,s) =
-      (case  Vartab.lookup (tye, v) of
-        Some U => norm_typ tye U
-      | None => TVar(v,s))
-  in map_type_tvar chase end
-
 fun typ_clash(tye,T,U) =
   if !trace_unify_fail
-  then let val t = Sign.string_of_typ (!sgr) (norm_typ tye T)
-           and u = Sign.string_of_typ (!sgr) (norm_typ tye U)
+  then let val t = Sign.string_of_typ (!sgr) (Envir.norm_type tye T)
+           and u = Sign.string_of_typ (!sgr) (Envir.norm_type tye U)
        in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   else ()