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