src/Sequents/prover.ML
 changeset 29269 5c25a2012975 parent 26928 ca87aff1ad2d child 32091 30e2ffbba718
```     1.1 --- a/src/Sequents/prover.ML	Wed Dec 31 00:08:14 2008 +0100
1.2 +++ b/src/Sequents/prover.ML	Wed Dec 31 15:30:10 2008 +0100
1.3 @@ -1,9 +1,8 @@
1.4 -(*  Title:      Sequents/prover
1.5 -    ID:         \$Id\$
1.6 +(*  Title:      Sequents/prover.ML
1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.8      Copyright   1992  University of Cambridge
1.9
1.10 -Simple classical reasoner for the sequent calculus, based on "theorem packs"
1.11 +Simple classical reasoner for the sequent calculus, based on "theorem packs".
1.12  *)
1.13
1.14
1.15 @@ -65,7 +64,7 @@
1.16    -- checks that each concl formula looks like some subgoal formula.
1.17    It SHOULD check order as well, using recursion rather than forall/exists*)
1.18  fun could_res (seqp,seqc) =
1.19 -      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc))
1.20 +      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
1.21                                (forms_of_seq seqp))
1.22               (forms_of_seq seqc);
1.23
1.24 @@ -78,7 +77,7 @@
1.25  	  could_res (leftp,leftc) andalso could_res (rightp,rightc)
1.26      | (_ \$ Abs(_,_,leftp) \$ rightp,
1.27         _ \$ Abs(_,_,leftc) \$ rightc) =>
1.28 -	  could_res (leftp,leftc)  andalso  could_unify (rightp,rightc)
1.29 +	  could_res (leftp,leftc)  andalso  Term.could_unify (rightp,rightc)
1.30      | _ => false;
1.31
1.32
```