# HG changeset patch
# User wenzelm
# Date 1005845784 -3600
# Node ID 264f17d14ad9c221052a6c7161f4d6bcbf37bcaf
# Parent  657ad5edeab608da5751fd8d1adb70b34a9ccb53
fix_frees: rev;

diff -r 657ad5edeab6 -r 264f17d14ad9 src/Pure/Isar/proof_context.ML
--- 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!*)