src/Pure/old_goals.ML
changeset 22360 26ead7ed4f4b
parent 22109 9188aed2c3ca
child 22675 acf10be7dcca
     1.1 --- a/src/Pure/old_goals.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/Pure/old_goals.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -392,9 +392,9 @@
     1.4    (case  Seq.pull(tac th)  of
     1.5       NONE      => error"by: tactic failed"
     1.6     | SOME(th2,ths2) =>
     1.7 -       (if eq_thm(th,th2)
     1.8 +       (if Thm.eq_thm(th,th2)
     1.9            then warning "Warning: same as previous level"
    1.10 -          else if eq_thm_thy(th,th2) then ()
    1.11 +          else if Thm.eq_thm_thy(th,th2) then ()
    1.12            else warning ("Warning: theory of proof state has changed" ^
    1.13                         thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
    1.14         ((th2,ths2)::(th,ths)::pairs)));
    1.15 @@ -414,9 +414,9 @@
    1.16       (case Seq.pull thstr of
    1.17            NONE      => (writeln"Going back a level..."; backtrack pairs)
    1.18          | SOME(th2,thstr2) =>
    1.19 -           (if eq_thm(th,th2)
    1.20 +           (if Thm.eq_thm(th,th2)
    1.21                then warning "Warning: same as previous choice at this level"
    1.22 -              else if eq_thm_thy(th,th2) then ()
    1.23 +              else if Thm.eq_thm_thy(th,th2) then ()
    1.24                else warning "Warning: theory of proof state has changed";
    1.25              (th2,thstr2)::pairs));
    1.26