src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Sat Mar 07 15:40:36 2015 +0100
+++ b/src/FOL/simpdata.ML	Sat Mar 07 21:32:31 2015 +0100
@@ -50,7 +50,8 @@
        | _ => [th])
   in atoms end;
 
-fun mksimps pairs (_: Proof.context) = map mk_eq o mk_atomize pairs o gen_all;
+fun mksimps pairs ctxt =
+  map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt);
 
 
 (** make simplification procedures for quantifier elimination **)