src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

 (* some peephole optimisations *)
 
 fun peephole_optimisation thy intro =
   let
     val process =
-      Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
+      rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
     fun process_False intro_t =
       if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
     fun process_True intro_t =
       map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
   in