src/Provers/classical.ML
changeset 46459 73823dbbecc4
parent 45375 7fe19930dfc9
child 46874 993c413746f4
     1.1 --- a/src/Provers/classical.ML	Tue Feb 14 16:59:12 2012 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Feb 14 17:11:33 2012 +0100
     1.3 @@ -670,8 +670,8 @@
     1.4  fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
     1.5  fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
     1.6  
     1.7 -fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
     1.8 -fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
     1.9 +fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
    1.10 +fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
    1.11  fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
    1.12  fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
    1.13