src/Pure/Isar/method.ML
changeset 8613 ec9ba98587a9
parent 8537 8abfc72109f2
child 8671 6ce91a80f616
     1.1 --- a/src/Pure/Isar/method.ML	Thu Mar 30 14:21:28 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Mar 30 14:22:15 2000 +0200
     1.3 @@ -346,10 +346,10 @@
     1.4  
     1.5  fun tactic txt ctxt = METHOD (fn facts =>
     1.6   (Context.use_mltext
     1.7 -   ("let fun (tactic: Proof.context -> thm list -> tactic) ctxt facts = \
     1.8 -    \let val thm = ProofContext.get_thm ctxt and thms = ProofContext.get_thms ctxt in\n"
     1.9 +   ("let fun (tactic: PureIsar.Proof.context -> thm list -> tactic) ctxt facts = \
    1.10 +    \let val thm = PureIsar.ProofContext.get_thm ctxt and thms = PureIsar.ProofContext.get_thms ctxt in\n"
    1.11      ^ txt ^
    1.12 -    "\nend in Method.set_tactic tactic end")
    1.13 +    "\nend in PureIsar.Method.set_tactic tactic end")
    1.14    false (Some (ProofContext.theory_of ctxt)); ! tactic_ref ctxt facts));
    1.15  
    1.16