# HG changeset patch
# User wenzelm
# Date 936716248 -7200
# Node ID 0fec518130794220be2167fd11a970b1c3f1b6c6
# Parent  e8be98558eb810b575e78ed7db535fe8b57c94c1
then_tac = refine;

diff -r e8be98558eb8 -r 0fec51813079 src/Pure/Isar/method.ML
--- 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 *)