src/Pure/Isar/expression.ML

     val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;
 
     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
-      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
+      rewrite_goals_tac [pred_def] THEN
       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
       Tactic.compose_tac (false,
         Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq,
-        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
+        Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_balanced (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness defs_ctxt t
-       (MetaSimplifier.rewrite_goals_tac defs THEN
+       (rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 in