src/Pure/Isar/local_defs.ML

 
 (* meta rewrite rules *)
 
 fun meta_rewrite_conv ctxt =
   Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
-    (empty_simpset ctxt
-      addsimps (Rules.get (Context.Proof ctxt))
+    (ctxt
+      |> Raw_Simplifier.init_simpset (Rules.get (Context.Proof ctxt))
       |> Raw_Simplifier.add_eqcong Drule.equals_cong);    (*protect meta-level equality*)
 
 val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
 
 fun abs_def_rule ctxt = meta_rewrite_rule ctxt #> Drule.abs_def;