src/Pure/Isar/obtain.ML
changeset 20224 9c40a144ee0e
parent 20218 be3bfb0699ba
child 20308 ddb7e7129481
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Jul 27 13:43:00 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jul 27 13:43:01 2006 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4              val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
     1.5            in
     1.6              ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
     1.7 -            ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
     1.8 +            ctxt' |> ProofContext.add_assms_i Assumption.assume_export
     1.9                [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    1.10              |>> (fn [(_, [th])] => th)
    1.11            end;