--- 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;