src/HOL/Tools/TFL/rules.ML

      val dummy = ss_ref  := []
      val cut_lemma' = cut_lemma RS eq_reflection
      fun prover used ss thm =
      let fun cong_prover ss thm =
          let val dummy = say "cong_prover:"
-             val cntxt = MetaSimplifier.prems_of_ss ss
+             val cntxt = Simplifier.prems_of_ss ss
              val dummy = print_thms "cntxt:" cntxt
              val dummy = say "cong rule:"
              val dummy = say (Display.string_of_thm thm)
              val dummy = thm_ref := (thm :: !thm_ref)
              val dummy = ss_ref := (ss :: !ss_ref)

                  let val tych = cterm_of thy
                      val dummy = print_cterms "To eliminate:" [tych imp]
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
-                     val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss
+                     val ss' = Simplifier.add_prems (map ASSUME ants) ss
                      val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
                        handle U.ERR _ => Thm.reflexive lhs
                      val dummy = print_thms "proven:" [lhs_eq_lhs1]
                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq

                   val ants1 = map tych (Logic.strip_imp_prems imp_body1)
                   val eq1 = Logic.strip_imp_concl imp_body1
                   val Q = get_lhs eq1
                   val QeqQ1 = pbeta_reduce (tych Q)
                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
-                  val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
+                  val ss' = Simplifier.add_prems (map ASSUME ants1) ss
                   val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
                                 handle U.ERR _ => Thm.reflexive Q1
                   val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
                   val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)

          in SOME(eliminate (rename thm)) end
          handle U.ERR _ => NONE    (* FIXME handle THM as well?? *)
 
         fun restrict_prover ss thm =
           let val dummy = say "restrict_prover:"
-              val cntxt = rev(MetaSimplifier.prems_of_ss ss)
+              val cntxt = rev(Simplifier.prems_of_ss ss)
               val dummy = print_thms "cntxt:" cntxt
               val thy = Thm.theory_of_thm thm
               val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
               fun genl tm = let val vlist = subtract (op aconv) globals
                                            (OldTerm.add_term_frees(tm,[]))