src/HOL/W0/ROOT.ML

--- a/src/HOL/W0/ROOT.ML	Mon Feb 25 20:51:48 2002 +0100
+++ b/src/HOL/W0/ROOT.ML	Tue Feb 26 00:19:04 2002 +0100
@@ -1,13 +1,2 @@
-(*  Title:      HOL/W0/ROOT.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1995 TUM
 
-Type inference for let-free MiniML
-*)
-
-Unify.trace_bound := 20;
-
-AddSEs [less_SucE];
-
-time_use_thy "I";
+use_thy "W0";