# HG changeset patch
# User wenzelm
# Date 1362830484 -3600
# Node ID 50fb0f35a14f85de11e7fa942bb054f62e74bf3f
# Parent  51957d006677efdf2fe314f4ac4cdb8e675b3bd6
tuned;

diff -r 51957d006677 -r 50fb0f35a14f src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sat Mar 09 11:56:01 2013 +0100
+++ b/src/HOL/Tools/try0.ML	Sat Mar 09 13:01:24 2013 +0100
@@ -61,7 +61,7 @@
   method |> parse_method
          |> Method.method thy
          |> Method.Basic
-         |> curry Method.SelectGoals 1
+         |> curry Method.Select_Goals 1
          |> Proof.refine
   handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
 
diff -r 51957d006677 -r 50fb0f35a14f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat Mar 09 11:56:01 2013 +0100
+++ b/src/Pure/Isar/method.ML	Sat Mar 09 13:01:24 2013 +0100
@@ -53,7 +53,7 @@
     Orelse of text list |
     Try of text |
     Repeat1 of text |
-    SelectGoals of int * text
+    Select_Goals of int * text
   val primitive_text: (thm -> thm) -> text
   val succeed_text: text
   val default_text: text
@@ -289,7 +289,7 @@
   Orelse of text list |
   Try of text |
   Repeat1 of text |
-  SelectGoals of int * text;
+  Select_Goals of int * text;
 
 fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)));
 val succeed_text = Basic (K succeed);
@@ -407,7 +407,8 @@
 and meth3 x =
  (meth4 --| Parse.$$$ "?" >> Try ||
   meth4 --| Parse.$$$ "+" >> Repeat1 ||
-  meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]") >> (SelectGoals o swap) ||
+  meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]")
+    >> (Select_Goals o swap) ||
   meth4) x
 and meth2 x =
  (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
diff -r 51957d006677 -r 50fb0f35a14f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Mar 09 11:56:01 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 09 13:01:24 2013 +0100
@@ -404,9 +404,7 @@
   end;
 
 fun select_goals n meth state =
-  state
-  |> (#2 o #2 o get_goal)
-  |> ALLGOALS Goal.conjunction_tac
+  ALLGOALS Goal.conjunction_tac (#2 (#2 (get_goal state)))
   |> Seq.maps (fn goal =>
     state
     |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
@@ -426,7 +424,7 @@
       | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
       | eval (Method.Try txt) = Seq.TRY (eval txt)
       | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt)
-      | eval (Method.SelectGoals (n, txt)) = select_goals n (eval txt);
+      | eval (Method.Select_Goals (n, txt)) = select_goals n (eval txt);
   in eval text state end;
 
 in