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.
close_schematic_term: uniform order of types/terms;
authorwenzelm
Thu, 05 Mar 2009 17:09:07 +0100
changeset 30285 a135bfab6e83
parent 30284 907da436f8a9
child 30286 cf89a03ee308
close_schematic_term: uniform order of types/terms; tuned;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/term.ML	Thu Mar 05 15:27:07 2009 +0100
+++ b/src/Pure/term.ML	Thu Mar 05 17:09:07 2009 +0100
@@ -805,8 +805,8 @@
 fun close_schematic_term t =
   let
     val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
-    val extra_terms = map Var (rev (add_vars t []));
-  in fold_rev lambda (extra_types @ extra_terms) t end;
+    val extra_terms = map Var (add_vars t []);
+  in fold lambda (extra_terms @ extra_types) t end;
isabelle