src/Pure/Isar/method.ML
changeset 22086 cf6019fece63
parent 21962 279b129498b6
child 22118 16639b216295
     1.1 --- a/src/Pure/Isar/method.ML	Fri Jan 19 13:09:32 2007 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Jan 19 13:09:33 2007 +0100
     1.3 @@ -348,7 +348,7 @@
     1.4         ^ txt ^
     1.5         "\nend in Method.set_tactic tactic end")
     1.6      false NONE;
     1.7 -    Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));
     1.8 +    Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
     1.9  
    1.10  
    1.11  
    1.12 @@ -448,8 +448,9 @@
    1.13      "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
    1.14      \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
    1.15      \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    1.16 -    "Method.add_method method"
    1.17 -    ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
    1.18 +    "Context.map_theory (Method.add_method method)"
    1.19 +    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
    1.20 +  |> Context.theory_map;
    1.21  
    1.22  
    1.23