split multi-goals as usual (outermost Pure.conjunction only);

--- 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