--- a/src/Pure/tctical.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/tctical.ML Mon Feb 26 23:18:24 2007 +0100
@@ -160,7 +160,7 @@
| evyBack ((st',q,tacs)::trail) =
case Seq.pull q of
NONE => evyBack trail
- | SOME(st,q') => if eq_thm (st',st)
+ | SOME(st,q') => if Thm.eq_thm (st',st)
then evyBack ((st',q',tacs)::trail)
else EVY ((st,q',tacs)::trail, tacs) st
in
@@ -302,7 +302,7 @@
(*Accept only next states that change the theorem's prop field
(changes to signature, hyps, etc. don't count)*)
fun CHANGED_PROP tac st =
- let fun diff st' = not (Drule.eq_thm_prop (st, st'));
+ let fun diff st' = not (Thm.eq_thm_prop (st, st'));
in Seq.filter diff (tac st) end;