src/Pure/meta_simplifier.ML

     if null bs then ()
     else print_term true ("Simplifier: term contains loose bounds: " ^ commas_quote bs) ss
       (Thm.theory_of_cterm ct) (Thm.term_of ct)
   end);
 
-fun rewrite_cterm mode prover raw_ss ct =
-  let
+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;
     val _ = conditional (!simp_depth mod 20 = 0) (fn () =>
       warning ("Simplification depth " ^ string_of_int (! simp_depth)));