src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML

           val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
           val prems' = maps dest_conjunct_prem (take nargs prems)
           fun param_rewrite prem =
             param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
           val SOME rew_eq = find_first param_rewrite prems'
-          val param_prem' = Raw_Simplifier.rewrite_rule
+          val param_prem' = rewrite_rule
             (map (fn th => th RS @{thm eq_reflection})
               [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
             param_prem
         in
           rtac param_prem' 1