diff -r 5c0024338cef -r 261abc2e3155 src/FOLP/ROOT.ML
--- 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"];