# HG changeset patch
# User wenzelm
# Date 1435783069 -7200
# Node ID 5d13babbb3f610163f6fd1e11cb18afce2897e31
# Parent  9eefb9f3902125ae97021db36a894b60d98a7c8f
split multi-goals as usual (outermost Pure.conjunction only);

diff -r 9eefb9f39021 -r 5d13babbb3f6 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Jul 01 22:11:23 2015 +0200
+++ b/src/Pure/subgoal.ML	Wed Jul 01 22:37:49 2015 +0200
@@ -166,7 +166,9 @@
 fun gen_subgoal prep_atts raw_result_binding raw_prems_binding params state =
   let
     val _ = Proof.assert_backward state;
-    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state;
+
+    val state1 = state |> Proof.refine_insert [];
+    val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
 
     val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
     val (prems_binding, do_prems) =
@@ -199,7 +201,7 @@
       #> Proof.reset_facts
       #> Proof.enter_backward;
   in
-    state
+    state1
     |> Proof.enter_forward
     |> Proof.using_facts []
     |> Proof.begin_block