# HG changeset patch
# User wenzelm
# Date 949945227 -3600
# Node ID 9f0ff98f37f6e6c9fd3d8c1a0ee7d0931943f4bc
# Parent  b2a4a3d86b731e09224c69abcd2c23bbdef0eadf
refine_no_facts: recover goal_facts;

diff -r b2a4a3d86b73 -r 9f0ff98f37f6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Feb 07 18:39:53 2000 +0100
+++ b/src/Pure/Isar/method.ML	Mon Feb 07 18:40:27 2000 +0100
@@ -455,9 +455,12 @@
   in eval text state end;
 
 fun refine_no_facts text state =
-  state
-  |> Proof.goal_facts (K [])
-  |> refine text;
+  let val (_, (goal_facts, _)) = Proof.get_goal state in
+    state
+    |> Proof.goal_facts (K [])
+    |> refine text
+    |> Seq.map (Proof.goal_facts (K goal_facts))
+  end;
 
 
 (* structured proof steps *)