# HG changeset patch
# User wenzelm
# Date 950557322 -3600
# Node ID ac8ac0eba73836523a3eecf4c6020cf4b0f5471b
# Parent  a55484a9b19f42e54f0ab2f34d9b570ad8493e1f
proof step: reset goal_facts;

diff -r a55484a9b19f -r ac8ac0eba738 src/Pure/Isar/method.ML
--- 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));