# HG changeset patch
# User wenzelm
# Date 1236269347 -3600
# Node ID a135bfab6e834813668a496871d76fed92c92f65
# Parent  907da436f8a94951878c939afc33f55eb461dfc1
close_schematic_term: uniform order of types/terms;
tuned;

diff -r 907da436f8a9 -r a135bfab6e83 src/Pure/term.ML
--- 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;