src/Pure/Tools/nbe.ML

 (** data setup **)
 
 (* preproc and postproc attributes *)
 
 structure NBE_Rewrite = TheoryDataFun
-(struct
-  val name = "Pure/nbe";
+(
   type T = thm list * thm list
-
-  val empty = ([],[])
+  val empty = ([], []);
   val copy = I;
   val extend = I;
-
   fun merge _ ((pres1,posts1), (pres2,posts2)) =
     (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
-
-  fun print _ _ = ()
-end);
+);
 
 val _ =
   let
     fun map_data f = Context.mapping (NBE_Rewrite.map f) I;
     fun attr_pre (thy, thm) =

       ((map_data o apsnd) (insert Thm.eq_thm thm) thy, thm)
     val attr = Attrib.syntax (Scan.lift (Args.$$$ "pre" >> K attr_pre
       || Args.$$$ "post" >> K attr_post));
   in
     Context.add_setup (
-      NBE_Rewrite.init
-      #> Attrib.add_attributes
+      Attrib.add_attributes
           [("normal", attr, "declare rewrite theorems for normalization")]
     )
   end;
 
 fun the_pres thy =