# HG changeset patch
# User wenzelm
# Date 1159645171 -7200
# Node ID 0e25916068675640eec0b3ddc9f40941ba511036
# Parent  ac78eee049ce90a5c9bed657fbe404a0fcb21a53
statement: Variable.fix_frees;

diff -r ac78eee049ce -r 0e2591606867 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Sep 30 21:39:29 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Sat Sep 30 21:39:31 2006 +0200
@@ -341,14 +341,14 @@
           let
             val xs = map fst vars;
             val props = map fst propp;
-            val (parms, ctxt'') =
-              ctxt'
+            val (parms, _) = ctxt'
               |> fold Variable.declare_term props
               |> fold_map ProofContext.inferred_param xs;
             val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
           in
             ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
-            ctxt' |> ProofContext.add_assms_i Assumption.assume_export
+            ctxt' |> Variable.fix_frees asm
+            |> ProofContext.add_assms_i Assumption.assume_export
               [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
             |>> (fn [(_, [th])] => th)
           end;