src/HOL/MiniML/ROOT.ML
changeset 6349 f7750d816c21
parent 2525 477c05586286
child 9000 c20d58286a51
--- a/src/HOL/MiniML/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/MiniML/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
@@ -6,8 +6,6 @@
 Type inference for MiniML
 *)
 
-HOL_build_completed;    (*Make examples fail if HOL did*)
-
 writeln"Root file for HOL/MiniML";
 
 time_use_thy "W";