src/Pure/axclass.ML
changeset 15801 d2f5ca3c048d
parent 15705 b5edb9dcec9a
child 15853 68b615bc110e
     1.1 --- a/src/Pure/axclass.ML	Thu Apr 21 22:00:28 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Apr 21 22:02:06 2005 +0200
     1.3 @@ -29,10 +29,9 @@
     1.4    val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
     1.5    val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
     1.6    val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
     1.7 -  val setup: (theory -> theory) list
     1.8  end;
     1.9  
    1.10 -structure AxClass : AX_CLASS =
    1.11 +structure AxClass: AX_CLASS =
    1.12  struct
    1.13  
    1.14  
    1.15 @@ -192,6 +191,7 @@
    1.16  end;
    1.17  
    1.18  structure AxclassesData = TheoryDataFun(AxclassesArgs);
    1.19 +val _ = Context.add_setup [AxclassesData.init];
    1.20  val print_axclasses = AxclassesData.print;
    1.21  
    1.22  
    1.23 @@ -292,20 +292,13 @@
    1.24    end;
    1.25  
    1.26  
    1.27 -(* intro_classes *)
    1.28 +(* proof methods *)
    1.29  
    1.30  fun intro_classes_tac facts st =
    1.31    (ALLGOALS (Method.insert_tac facts THEN'
    1.32        REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
    1.33      THEN Tactic.distinct_subgoals_tac) st;
    1.34  
    1.35 -val intro_classes_method =
    1.36 -  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    1.37 -    "back-chain introduction rules of axiomatic type classes");
    1.38 -
    1.39 -
    1.40 -(* default method *)
    1.41 -
    1.42  fun default_intro_classes_tac [] = intro_classes_tac []
    1.43    | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
    1.44  
    1.45 @@ -313,8 +306,10 @@
    1.46    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    1.47      default_intro_classes_tac facts;
    1.48  
    1.49 -val default_method =
    1.50 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
    1.51 +val _ = Context.add_setup [Method.add_methods
    1.52 + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    1.53 +   "back-chain introduction rules of axiomatic type classes"),
    1.54 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
    1.55  
    1.56  
    1.57  (* old-style axclass_tac *)
    1.58 @@ -419,16 +414,6 @@
    1.59  val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
    1.60  
    1.61  
    1.62 -
    1.63 -(** package setup **)
    1.64 -
    1.65 -(* setup theory *)
    1.66 -
    1.67 -val setup =
    1.68 - [AxclassesData.init,
    1.69 -  Method.add_methods [intro_classes_method, default_method]];
    1.70 -
    1.71 -
    1.72  (* outer syntax *)
    1.73  
    1.74  local structure P = OuterParse and K = OuterSyntax.Keyword in
    1.75 @@ -450,4 +435,3 @@
    1.76  end;
    1.77  
    1.78  end;
    1.79 -