src/Pure/Isar/method.ML

     Then of text list |
     Orelse of text list |
     Try of text |
     Repeat1 of text |
     Select_Goals of int * text
-  val primitive_text: (thm -> thm) -> text
+  val primitive_text: (Proof.context -> thm -> thm) -> text
   val succeed_text: text
   val default_text: text
   val this_text: text
   val done_text: text
   val sorry_text: bool -> text

   Orelse of text list |
   Try of text |
   Repeat1 of text |
   Select_Goals of int * text;
 
-fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)));
+fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
 val succeed_text = Basic (K succeed);
 val default_text = Source (Args.src (("default", []), Position.none));
 val this_text = Basic (K this);
 val done_text = Basic (K (SIMPLE_METHOD all_tac));
 fun sorry_text int = Basic (fn ctxt => cheating ctxt int);