diff -r 6ec0c8f9d68d -r 7239b21e2068 src/ZF/ROOT.ML --- 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";