src/HOL/Isar_examples/ExprCompiler.thy

--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Apr 27 10:45:20 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Apr 27 10:46:37 1999 +0200
@@ -101,7 +101,6 @@
   @{term "comp"}.  We first establish some lemmas.
 |};
 
-ML "reset HOL_quantifiers";
 
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");