src/HOL/Predicate.thy
changeset 22846 fb79144af9a3
parent 22430 6a56bf1b3a64
child 23389 aaca6a8e5414
     1.1 --- a/src/HOL/Predicate.thy	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -152,14 +152,12 @@
     1.4  val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
     1.5  
     1.6  structure PredSetConvData = GenericDataFun
     1.7 -(struct
     1.8 -  val name = "HOL/pred_set_conv";
     1.9 +(
    1.10    type T = thm list;
    1.11    val empty = [];
    1.12    val extend = I;
    1.13    fun merge _ = Drule.merge_rules;
    1.14 -  fun print _ _ = ()
    1.15 -end)
    1.16 +);
    1.17  
    1.18  fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
    1.19    Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
    1.20 @@ -170,7 +168,7 @@
    1.21  
    1.22  in
    1.23  
    1.24 -val _ = ML_Context.>> (PredSetConvData.init #>
    1.25 +val _ = ML_Context.>> (
    1.26    Attrib.add_attributes
    1.27      [("pred_set_conv", pred_set_conv_att,
    1.28          "declare rules for converting between predicate and set notation"),