--- a/src/ZF/OrdQuant.thy Sat Mar 29 19:13:58 2008 +0100
+++ b/src/ZF/OrdQuant.thy Sat Mar 29 19:14:00 2008 +0100
@@ -369,7 +369,7 @@
text {* Setting up the one-point-rule simproc *}
-ML_setup {*
+ML {*
local
val unfold_rex_tac = unfold_tac [@{thm rex_def}];