1.1 --- a/src/Pure/Isar/obtain.ML	Thu Nov 29 01:50:50 2001 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Nov 29 01:51:06 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, [Method.intro_local]), [(that_prop, ([], []))])]
     1.8 +    |> Proof.assume_i [((thatN, [RuleContext.intro_query_local None]), [(that_prop, ([], []))])]
     1.9      |> (fn state' =>
    1.10        state'
    1.11        |> Proof.from_facts chain_facts