Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Type.norm_term;
authorwenzelm
Fri, 23 Jul 1999 16:51:25 +0200
changeset 7068 d396d8b935f1
parent 7067 601f930d3739
child 7069 f54023a6c7e2
Type.norm_term;
src/Pure/sign.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle