src/ZF/ROOT.ML
changeset 8812 7239b21e2068
parent 8127 68c6159440f1
child 9176 8f975d9c1046
--- a/src/ZF/ROOT.ML	Fri May 05 22:24:47 2000 +0200
+++ b/src/ZF/ROOT.ML	Fri May 05 22:25:17 2000 +0200
@@ -16,7 +16,6 @@
 print_depth 1;
 
 (*Add user sections for inductive/datatype definitions*)
-use     "~~/src/Pure/section_utils";
 use     "thy_syntax";
 
 use_thy "Let";