# HG changeset patch
# User wenzelm
# Date 932741485 -7200
# Node ID d396d8b935f1de777ca0728058c97b0521c29909
# Parent  601f930d373973a832761c757029aff5e12088df
Type.norm_term;

diff -r 601f930d3739 -r d396d8b935f1 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Jul 23 16:50:55 1999 +0200
+++ b/src/Pure/sign.ML	Fri Jul 23 16:51:25 1999 +0200
@@ -655,7 +655,7 @@
 
     val norm_tm =
       (case it_term_types (Type.typ_errors tsig) (tm, []) of
-        [] => map_term_types (Type.norm_typ tsig) tm
+        [] => Type.norm_term tsig tm
       | errs => raise TYPE (cat_lines errs, [], [tm]));
     val _ = nodup_Vars norm_tm;
   in