diff -r 19b47bfac6ef -r 9e7d1c139569 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Apr 18 17:07:01 2013 +0200
@@ -191,7 +191,7 @@
 
 fun meta_rewrite_conv ctxt =
   Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
-    (Raw_Simplifier.context ctxt empty_ss
+    (empty_simpset ctxt
       addsimps (Rules.get (Context.Proof ctxt))
       |> Raw_Simplifier.add_eqcong Drule.equals_cong);    (*protect meta-level equality*)