diff -r 5212516f1a98 -r 113dbd65319e src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Feb 15 21:35:02 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Feb 15 21:35:02 2006 +0100
@@ -1157,8 +1157,9 @@
       (Thm.theory_of_cterm ct) (Thm.term_of ct)
   end);
 
-fun rewrite_cterm mode prover raw_ss ct =
+fun rewrite_cterm mode prover raw_ss raw_ct =
   let
+    val ct = Thm.adjust_maxidx raw_ct;
     val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
     val ss = fallback_context thy raw_ss;
     val _ = inc simp_depth;