changeset 51717 | 9e7d1c139569 |
parent 51585 | fcd5af4aac2b |
child 54742 | 7a86358a3c0b |
--- 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*)