diff -r dd0f298b024c -r 477c05586286 src/HOL/MiniML/ROOT.ML
--- a/src/HOL/MiniML/ROOT.ML	Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/ROOT.ML	Fri Jan 17 18:50:04 1997 +0100
@@ -1,16 +1,13 @@
 (*  Title:      HOL/MiniML/ROOT.ML
     ID:         $Id$
-    Author:     Tobias Nipkow
+    Author:     Wolfgang Naraschewski and Tobias Nipkow
     Copyright   1995 TUM
 
-Type inference for let-free MiniML
+Type inference for MiniML
 *)
 
 HOL_build_completed;    (*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/MiniML";
-Unify.trace_bound := 20;
 
-AddSEs [less_SucE];
-
-time_use_thy "I";
+time_use_thy "W";