--- a/src/HOL/W0/ROOT.ML Tue May 30 16:03:09 2000 +0200 +++ b/src/HOL/W0/ROOT.ML Tue May 30 16:08:38 2000 +0200 @@ -6,8 +6,6 @@ Type inference for let-free MiniML *) -writeln"Root file for HOL/W0"; - Unify.trace_bound := 20; AddSEs [less_SucE];