src/HOL/Import/ROOT.ML

--- a/src/HOL/Import/ROOT.ML	Wed Jun 02 18:48:30 2010 +0200
+++ b/src/HOL/Import/ROOT.ML	Wed Jun 02 21:12:28 2010 +0200
@@ -1,8 +1,5 @@
 (*  Title:      HOL/Import/ROOT.ML
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-Proofterm.proofs := 0;
-use_thy "HOL4Compat";
-use_thy "HOL4Syntax";
+use_thys ["HOL4Compat", "HOL4Syntax"];