diff -r 5f9138bcb3d7 -r fb79144af9a3 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sun May 06 21:50:17 2007 +0200
+++ b/src/HOL/Predicate.thy	Mon May 07 00:49:59 2007 +0200
@@ -152,14 +152,12 @@
 val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
 
 structure PredSetConvData = GenericDataFun
-(struct
-  val name = "HOL/pred_set_conv";
+(
   type T = thm list;
   val empty = [];
   val extend = I;
   fun merge _ = Drule.merge_rules;
-  fun print _ _ = ()
-end)
+);
 
 fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
   Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
@@ -170,7 +168,7 @@
 
 in
 
-val _ = ML_Context.>> (PredSetConvData.init #>
+val _ = ML_Context.>> (
   Attrib.add_attributes
     [("pred_set_conv", pred_set_conv_att,
         "declare rules for converting between predicate and set notation"),