diff -r 5bf4a54ba25f -r 4a960c012383 src/HOL/MiniML/ROOT.ML
--- a/src/HOL/MiniML/ROOT.ML	Tue Nov 21 12:41:52 1995 +0100
+++ b/src/HOL/MiniML/ROOT.ML	Tue Nov 21 12:43:09 1995 +0100
@@ -9,9 +9,6 @@
 HOL_build_completed;	(*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/MiniML";
-loadpath := [".","MiniML"];
 Unify.trace_bound := 20;
 
 time_use_thy "I";
-
-make_chart ();   (*make HTML chart*)