src/Pure/Isar/method.ML
changeset 7504 0fec51813079
parent 7439 a1b3310b4985
child 7506 08a88d4ebd54
--- 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 *)