# HG changeset patch
# User wenzelm
# Date 950045310 -3600
# Node ID a541e261c660f2974ef4b85b36bf0ebe58b74978
# Parent  419157483fc94d2d80ccc08bb25d7c5b8212eb35
(then_)tac: assert_backward;

diff -r 419157483fc9 -r a541e261c660 src/Pure/Isar/isar_thy.ML
--- 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;