refine_no_facts: recover goal_facts;

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