--- a/src/Pure/Isar/isar_thy.ML Tue Feb 08 20:17:41 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML Tue Feb 08 22:28:30 2000 +0100
@@ -354,8 +354,8 @@
(* backward steps *)
-val tac = ProofHistory.applys o Method.refine_no_facts;
-val then_tac = ProofHistory.applys o Method.refine;
+fun tac m = ProofHistory.applys (Method.refine_no_facts m o Proof.assert_backward);
+fun then_tac m = ProofHistory.applys (Method.refine m o Proof.assert_backward);
val proof = ProofHistory.applys o Method.proof o
apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;