--- a/src/HOL/AxClasses/Tutorial/ROOT.ML Tue Aug 17 22:14:02 1999 +0200
+++ b/src/HOL/AxClasses/Tutorial/ROOT.ML Tue Aug 17 22:14:08 1999 +0200
@@ -7,7 +7,6 @@
example resides in directory FOL/ex/.)
*)
-reset HOL_quantifiers;
set show_types;
set show_sorts;