src/Pure/raw_simplifier.ML

--- a/src/Pure/raw_simplifier.ML	Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Jul 28 20:59:39 2015 +0200
@@ -1385,7 +1385,7 @@
     Conv.fconv_rule
       (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th)
   |> Thm.adjust_maxidx_thm ~1
-  |> Drule.gen_all (Variable.maxidx_of ctxt);
+  |> Variable.gen_all ctxt;
 
 val hhf_ss =
   simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))