proof step: reset goal_facts;

--- a/src/Pure/Isar/method.ML	Mon Feb 14 12:23:08 2000 +0100
+++ b/src/Pure/Isar/method.ML	Mon Feb 14 20:42:02 2000 +0100
@@ -496,6 +496,7 @@
   state
   |> Proof.assert_backward
   |> refine (if_none opt_text default_text)
+  |> Seq.map (Proof.goal_facts (K []))
   |> Seq.map Proof.enter_forward;
 
 fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));