diff -r 48d400469bcb -r c6f413b660cf src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sat Mar 07 15:40:36 2015 +0100
+++ b/src/ZF/OrdQuant.thy	Sat Mar 07 21:32:31 2015 +0100
@@ -361,7 +361,8 @@
     ZF_conn_pairs, ZF_mem_pairs);
 *}
 declaration {* fn _ =>
-  Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all)))
+  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
+    map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt)))
 *}
 
 text {* Setting up the one-point-rule simproc *}