then_tac = refine;

--- a/src/Pure/Isar/method.ML	Tue Sep 07 16:57:15 1999 +0200
+++ b/src/Pure/Isar/method.ML	Tue Sep 07 16:57:28 1999 +0200
@@ -347,10 +347,7 @@
   |> Proof.goal_facts (K [])
   |> refine text;
 
-fun then_tac text state =
-  state
-  |> Proof.goal_facts Proof.the_facts
-  |> refine text;
+val then_tac = refine;
 
 
 (* structured proof steps *)