--- a/src/Pure/Isar/isar_thy.ML Tue Sep 07 16:57:52 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML Tue Sep 07 17:21:44 1999 +0200
@@ -326,8 +326,8 @@
(* backward steps *)
-val tac = ProofHistory.applys o Method.tac;
-val then_tac = ProofHistory.applys o Method.then_tac;
+val tac = ProofHistory.applys o Method.refine_no_facts;
+val then_tac = ProofHistory.applys o Method.refine;
val proof = ProofHistory.applys o Method.proof o
apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;