proper state after qed;

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