diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Sequents/modal.ML
--- a/src/Sequents/modal.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Sequents/modal.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,9 +1,8 @@
 (*  Title:      Sequents/modal.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Simple modal reasoner
+Simple modal reasoner.
 *)
 
 
@@ -39,7 +38,7 @@
   Assumes each formula in seqc is surrounded by sequence variables
   -- checks that each concl formula looks like some subgoal formula.*)
 fun could_res (seqp,seqc) =
-      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
+      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
                               (forms_of_seq seqp))
              (forms_of_seq seqc);