src/Pure/Isar/attrib.ML

   val local_thmss: ProofContext.context * Args.T list -> thm list * (ProofContext.context * Args.T list)
   val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute
   val no_args: 'a attribute -> src -> 'a attribute
   val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
   val attribute: (theory attribute * ProofContext.context attribute) -> src
-  val setup: (theory -> theory) list
 end;
 
 structure Attrib: ATTRIB =
 struct
 

       |> Pretty.chunks |> Pretty.writeln
     end;
 end;
 
 structure AttributesData = TheoryDataFun(AttributesDataArgs);
+val _ = Context.add_setup [AttributesData.init];
 val print_attributes = AttributesData.print;
 
 
 (* interning *)
 

 fun attribute att = Args.src ((attributeN, [Args.mk_attribute att]), Position.none);
 
 fun attribute_global x = (syntax (Scan.lift Args.internal_attribute >> #1)) x;
 fun attribute_local x = (syntax (Scan.lift Args.internal_attribute >> #2)) x;
 
-val setup_internal_attribute =
+val _ = Context.add_setup
  [PureThy.global_path,
   add_attributes [(attributeN, (attribute_global, attribute_local), "internal attribute")],
   PureThy.local_path];
 
-
-
-(** theory setup **)
 
 (* pure_attributes *)
 
 val pure_attributes =
  [("tagged", (gen_tagged, gen_tagged), "tagged theorem"),

   ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
     "declaration of rulify rule"),
   ("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")] @
   rule_atts;
 
-
-(* setup *)
-
-val setup =
- AttributesData.init :: setup_internal_attribute @ [add_attributes pure_attributes];
+val _ = Context.add_setup [add_attributes pure_attributes];
+
 
 end;
 
 structure BasicAttrib: BASIC_ATTRIB = Attrib;
 open BasicAttrib;
-