--- a/src/HOL/ROOT.ML Wed Oct 25 09:46:46 1995 +0100 +++ b/src/HOL/ROOT.ML Wed Oct 25 09:48:29 1995 +0100 @@ -11,7 +11,6 @@ writeln banner; print_depth 1; -set eta_contract; (* Add user sections *) use "../Pure/section_utils.ML";