diff -r 26685edee372 -r a509730e424b src/HOL/AxClasses/Tutorial/ROOT.ML
--- 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;