# HG changeset patch
# User wenzelm
# Date 1205775364 -3600
# Node ID 2f387f5c0f52a531c97fa788325557c3d57375e5
# Parent  53e382ccf71fc99a0df68de598b94687325b6ffc
closeup: recover original order of free variables!

diff -r 53e382ccf71f -r 2f387f5c0f52 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Mar 17 16:47:45 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 17 18:36:04 2008 +0100
@@ -1227,7 +1227,7 @@
             val rev_frees =
               Term.fold_aterms (fn Free (x, T) =>
                 if Variable.is_fixed ctxt x then I else insert (op =) (x, T) | _ => I) t [];
-          in Term.list_all_free (rev_frees, t) end;
+          in Term.list_all_free (rev rev_frees, t) end;
 
         fun no_binds [] = []
           | no_binds _ = error "Illegal term bindings in locale element";