--- a/src/FOLP/ROOT.ML Wed Nov 11 09:02:37 2009 +0100
+++ b/src/FOLP/ROOT.ML Wed Nov 11 14:15:11 2009 +0100
@@ -1,6 +1,5 @@
(* Title: FOLP/ROOT.ML
- ID: $Id$
- Author: martin Coen, Cambridge University Computer Laboratory
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Modifed version of Lawrence Paulson's FOL that contains proof terms.
@@ -8,5 +7,5 @@
Presence of unknown proof term means that matching does not behave as expected.
*)
-use_thy "FOLP";
+use_thys ["FOLP"];