diff -r 0f1a583457da -r 1150f128c7fe src/HOL/MiniML/ROOT.ML
--- a/src/HOL/MiniML/ROOT.ML	Tue Aug 20 12:23:13 1996 +0200
+++ b/src/HOL/MiniML/ROOT.ML	Tue Aug 20 12:32:16 1996 +0200
@@ -11,4 +11,6 @@
 writeln"Root file for HOL/MiniML";
 Unify.trace_bound := 20;
 
+AddSEs [less_SucE];
+
 time_use_thy "I";