src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/FOL/simpdata.ML	Tue Jul 28 20:59:39 2015 +0200
@@ -50,8 +50,7 @@
        | _ => [th])
   in atoms end;
 
-fun mksimps pairs ctxt =
-  map mk_eq o mk_atomize pairs o Drule.gen_all (Variable.maxidx_of ctxt);
+fun mksimps pairs ctxt = map mk_eq o mk_atomize pairs o Variable.gen_all ctxt;
 
 
 (** make simplification procedures for quantifier elimination **)