statement: Variable.fix_frees;
authorwenzelm
Sat Sep 30 21:39:31 2006 +0200 (2006-09-30)
changeset 208040e2591606867
parent 20803 ac78eee049ce
child 20805 35574b9b59aa
statement: Variable.fix_frees;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Sat Sep 30 21:39:29 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sat Sep 30 21:39:31 2006 +0200
     1.3 @@ -341,14 +341,14 @@
     1.4            let
     1.5              val xs = map fst vars;
     1.6              val props = map fst propp;
     1.7 -            val (parms, ctxt'') =
     1.8 -              ctxt'
     1.9 +            val (parms, _) = ctxt'
    1.10                |> fold Variable.declare_term props
    1.11                |> fold_map ProofContext.inferred_param xs;
    1.12              val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
    1.13            in
    1.14              ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
    1.15 -            ctxt' |> ProofContext.add_assms_i Assumption.assume_export
    1.16 +            ctxt' |> Variable.fix_frees asm
    1.17 +            |> ProofContext.add_assms_i Assumption.assume_export
    1.18                [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    1.19              |>> (fn [(_, [th])] => th)
    1.20            end;