src/Pure/Isar/local_defs.ML
changeset 24039 273698405054
parent 23541 f8c5e218e4d8
child 24261 dd31811bdf46
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sun Jul 29 14:29:52 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Jul 29 14:29:54 2007 +0200
     1.3 @@ -151,15 +151,15 @@
     1.4    type T = thm list;
     1.5    val empty = []
     1.6    val extend = I;
     1.7 -  fun merge _ = Drule.merge_rules;
     1.8 +  fun merge _ = Thm.merge_thms;
     1.9  );
    1.10  
    1.11  fun print_rules ctxt =
    1.12    Pretty.writeln (Pretty.big_list "definitional transformations:"
    1.13      (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
    1.14  
    1.15 -val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
    1.16 -val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
    1.17 +val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
    1.18 +val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
    1.19  
    1.20  
    1.21  (* meta rewrite rules *)