src/Pure/Isar/obtain.ML
changeset 12350 5fad0e7129c3
parent 12325 4966dae8fa62
child 12404 968213967c07
     1.1 --- a/src/Pure/Isar/obtain.ML	Mon Dec 03 21:03:06 2001 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Mon Dec 03 21:31:55 2001 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4      |> Proof.enter_forward
     1.5      |> Proof.begin_block
     1.6      |> Proof.fix_i [([thesisN], None)]
     1.7 -    |> Proof.assume_i [((thatN, [RuleContext.intro_query_local None]), [(that_prop, ([], []))])]
     1.8 +    |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])]
     1.9      |> (fn state' =>
    1.10        state'
    1.11        |> Proof.from_facts chain_facts