--- a/src/Pure/Isar/local_defs.ML Wed Nov 23 22:07:55 2011 +0100
+++ b/src/Pure/Isar/local_defs.ML Wed Nov 23 22:59:39 2011 +0100
@@ -217,8 +217,8 @@
fun meta_rewrite_conv ctxt =
Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
(Raw_Simplifier.context ctxt empty_ss
- addeqcongs [Drule.equals_cong] (*protect meta-level equality*)
- addsimps (Rules.get (Context.Proof ctxt)));
+ addsimps (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;