# HG changeset patch
# User wenzelm
# Date 1129327686 -7200
# Node ID 810a67ecbc6431cb627bb85b263226da150ea646
# Parent  0551978bfda575d633fa9941ee43a7e00cf46870
added primitive_text, succeed_text;

diff -r 0551978bfda5 -r 810a67ecbc64 src/Pure/Isar/method.ML
--- 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));