src/Pure/axclass.ML

   val axclass_tac: thm list -> tactic
   val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
   val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
   val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
   val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
-  val setup: (theory -> theory) list
 end;
 
-structure AxClass : AX_CLASS =
+structure AxClass: AX_CLASS =
 struct
 
 
 (** utilities **)
 

         [pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
     in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
 end;
 
 structure AxclassesData = TheoryDataFun(AxclassesArgs);
+val _ = Context.add_setup [AxclassesData.init];
 val print_axclasses = AxclassesData.print;
 
 
 (* get and put data *)
 

     map (Thm.class_triv sign) classes @
     List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes
   end;
 
 
-(* intro_classes *)
+(* proof methods *)
 
 fun intro_classes_tac facts st =
   (ALLGOALS (Method.insert_tac facts THEN'
       REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
     THEN Tactic.distinct_subgoals_tac) st;
 
-val intro_classes_method =
-  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
-    "back-chain introduction rules of axiomatic type classes");
-
-
-(* default method *)
-
 fun default_intro_classes_tac [] = intro_classes_tac []
   | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
 
 fun default_tac rules ctxt facts =
   HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
     default_intro_classes_tac facts;
 
-val default_method =
-  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
+val _ = Context.add_setup [Method.add_methods
+ [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+   "back-chain introduction rules of axiomatic type classes"),
+  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
 
 
 (* old-style axclass_tac *)
 
 (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",

   inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
 val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
 val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
 
 
-
-(** package setup **)
-
-(* setup theory *)
-
-val setup =
- [AxclassesData.init,
-  Method.add_methods [intro_classes_method, default_method]];
-
-
 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val axclassP =

 val _ = OuterSyntax.add_parsers [axclassP, instanceP];
 
 end;
 
 end;
-