# HG changeset patch
# User wenzelm
# Date 1435780641 -7200
# Node ID f64658887a0544e26120951b623f5940c738c50d
# Parent  5b6552e12421e407f84ae1b31205b14dfbbc1013
proper state after qed;

diff -r 5b6552e12421 -r f64658887a05 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Jul 01 21:48:46 2015 +0200
+++ b/src/Pure/subgoal.ML	Wed Jul 01 21:57:21 2015 +0200
@@ -190,7 +190,9 @@
             |> Seq.hd)
           |> Proof.map_context
             (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
-        end);
+        end)
+      #> Proof.reset_facts
+      #> Proof.enter_backward;
   in
     state
     |> Proof.enter_forward