fix_frees: rev;

--- a/src/Pure/Isar/proof_context.ML	Thu Nov 15 18:36:07 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 15 18:36:24 2001 +0100
@@ -1112,7 +1112,7 @@
   let
     val frees = foldl Drule.add_frees ([], ts);
     fun new (x, T) = if is_fixed ctxt x then None else Some ([x], Some T);
-  in fix_direct (mapfilter new frees) ctxt end;
+  in fix_direct (rev (mapfilter new frees)) ctxt end;
 
 
 (*Note: improper use may result in variable capture / dynamic scoping!*)