src/Pure/Isar/code_unit.ML

   val assert_rew: thm -> thm
   val mk_rew: thm -> thm
   val mk_func: thm -> thm
   val head_func: thm -> string * ((string * sort) list * typ)
   val expand_eta: int -> thm -> thm
-  val rewrite_func: MetaSimplifier.simpset -> thm -> thm
+  val rewrite_func: simpset -> thm -> thm
+  val rewrite_head: thm list -> thm -> thm
   val norm_args: thm list -> thm list 
   val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list
 
   (*case certificates*)
   val case_cert: thm -> string * (int * string list)

     fun lhs_conv ct = if can Thm.dest_comb ct
       then (Conv.fun_conv lhs_conv) ct
       else conv ct;
   in Conv.fun_conv (Conv.arg_conv lhs_conv) end;
 
-fun rewrite_func ss thm = (Conv.fconv_rule o func_conv o
-  (MetaSimplifier.rewrite' (ProofContext.init (Thm.theory_of_thm thm)) false)) ss thm;
+val rewrite_func = Conv.fconv_rule o func_conv o Simplifier.rewrite;
 val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false;
 
 fun norm_args thms =
   let
     val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;