added primitive_text, succeed_text;

--- a/src/Pure/Isar/method.ML	Sat Oct 15 00:08:05 2005 +0200
+++ b/src/Pure/Isar/method.ML	Sat Oct 15 00:08:06 2005 +0200
@@ -63,6 +63,8 @@
     Orelse of text list |
     Try of text |
     Repeat1 of text
+  val primitive_text: (thm -> thm) -> text
+  val succeed_text: text
   val default_text: text
   val this_text: text
   val done_text: text
@@ -522,6 +524,8 @@
   Try of text |
   Repeat1 of text;
 
+val primitive_text = Basic o K o SIMPLE_METHOD o PRIMITIVE;
+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));