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