src/Pure/Isar/local_defs.ML
changeset 26424 a6cad32a27b0
parent 25119 192105867f25
child 28083 103d9282a946
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Mar 27 14:41:07 2008 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Mar 27 14:41:09 2008 +0100
     1.3 @@ -203,13 +203,11 @@
     1.4  
     1.5  (* meta rewrite rules *)
     1.6  
     1.7 -val equals_ss =
     1.8 -  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
     1.9 -    addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
    1.10 -
    1.11  fun meta_rewrite_conv ctxt =
    1.12    MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
    1.13 -    (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
    1.14 +    (MetaSimplifier.context ctxt MetaSimplifier.empty_ss
    1.15 +      addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
    1.16 +      addsimps (Rules.get (Context.Proof ctxt)));
    1.17  
    1.18  val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
    1.19