src/Pure/raw_simplifier.ML

--- a/src/Pure/raw_simplifier.ML	Sat Mar 07 15:40:36 2015 +0100
+++ b/src/Pure/raw_simplifier.ML	Sat Mar 07 21:32:31 2015 +0100
@@ -1382,7 +1382,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;
+  |> Drule.gen_all (Variable.maxidx_of ctxt);
 
 val hhf_ss =
   simpset_of (empty_simpset (Context.proof_of (Context.the_thread_data ()))