src/Pure/Isar/element.ML

 fun pretty_statement ctxt kind raw_th =
   let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
-    val th = MetaSimplifier.norm_hhf raw_th;
+    val th = Raw_Simplifier.norm_hhf raw_th;
     val is_elim = Object_Logic.is_elim th;
 
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;

       (Conv.fconv_rule Drule.beta_eta_conversion
         (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
   end;
 
 fun conclude_witness (Witness (_, th)) =
-  Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
+  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th));
 
 fun pretty_witness ctxt witn =
   let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
     Pretty.block (prt_term (witness_prop witn) ::
       (if Config.get ctxt show_hyps then [Pretty.brk 2, Pretty.list "[" "]"

 (* rewriting with equalities *)
 
 fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
  {binding = I,
   typ = I,
-  term = MetaSimplifier.rewrite_term thy thms [],
-  fact = map (MetaSimplifier.rewrite_rule thms)});
+  term = Raw_Simplifier.rewrite_term thy thms [],
+  fact = map (Raw_Simplifier.rewrite_rule thms)});
 
 
 (* transfer to theory using closure *)
 
 fun transfer_morphism thy =