# HG changeset patch
# User wenzelm
# Date 1141503010 -3600
# Node ID 1bf4b5c4a794db968fa1f45e28a1b2c2710b3e1c
# Parent  9fb741abb008c62d944434e55d238bdf3991ef68
text: added SelectGoals;

diff -r 9fb741abb008 -r 1bf4b5c4a794 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Mar 04 21:10:09 2006 +0100
+++ b/src/Pure/Isar/method.ML	Sat Mar 04 21:10:10 2006 +0100
@@ -61,7 +61,8 @@
     Then of text list |
     Orelse of text list |
     Try of text |
-    Repeat1 of text
+    Repeat1 of text |
+    SelectGoals of int * text
   val primitive_text: (thm -> thm) -> text
   val succeed_text: text
   val default_text: text
@@ -507,7 +508,8 @@
   Then of text list |
   Orelse of text list |
   Try of text |
-  Repeat1 of text;
+  Repeat1 of text |
+  SelectGoals of int * text;
 
 val primitive_text = Basic o K o SIMPLE_METHOD o PRIMITIVE;
 val succeed_text = Basic (K succeed);
@@ -619,10 +621,10 @@
 fun sect ss = Scan.first (map Scan.lift ss);
 fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> List.concat;
 
-fun apply (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
+fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
 
 fun section ss = (sect ss -- thms ss) :-- (fn (m, ths) => Scan.depend (fn context =>
-  Scan.succeed (apply m (context, ths)))) >> #2;
+  Scan.succeed (app m (context, ths)))) >> #2;
 
 fun sectioned args ss = args -- Scan.repeat (section ss);