# HG changeset patch
# User wenzelm
# Date 1141839451 -3600
# Node ID a32d9dbe95513682874445996d26b42eb4501632
# Parent  ccdaf84bab5902e6fdce99ee4fe8dff45a893de6
select_goals: split original conjunctions;

diff -r ccdaf84bab59 -r a32d9dbe9551 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Mar 08 18:37:30 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 08 18:37:31 2006 +0100
@@ -412,15 +412,16 @@
   end;
 
 fun select_goals n meth state =
-  let val goal = #2 (#2 (get_goal state)) in
+  state
+  |> (#2 o #2 o get_goal)
+  |> ALLGOALS Tactic.conjunction_tac
+  |> Seq.maps (fn goal =>
     state
-    |> Seq.lift set_goal
-      (Seq.maps (Tactic.precise_conjunction_tac 1 n) (Goal.extract 1 n goal))
+    |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Tactic.conjunction_tac 1))
     |> Seq.maps meth
     |> Seq.maps (fn state' => state'
       |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
-    |> Seq.maps (apply_method true (K Method.succeed))
-  end;
+    |> Seq.maps (apply_method true (K Method.succeed)));
 
 fun apply_text cc text state =
   let