--- 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";