sane internal interfaces for instance;
authorwenzelm
Thu Oct 18 21:02:26 2001 +0200 (2001-10-18 ago)
changeset 11828ef3e51b1b4ec
parent 11827 16ef206e6648
child 11829 f252646080fc
sane internal interfaces for instance;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Thu Oct 18 21:01:59 2001 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Oct 18 21:02:26 2001 +0200
     1.3 @@ -16,14 +16,14 @@
     1.4      -> theory -> theory * {intro: thm, axioms: thm list}
     1.5    val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
     1.6      -> theory -> theory * {intro: thm, axioms: thm list}
     1.7 -  val add_inst_subclass: xclass * xclass -> string list -> thm list
     1.8 -    -> tactic option -> theory -> theory
     1.9 -  val add_inst_subclass_i: class * class -> string list -> thm list
    1.10 +  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
    1.11      -> tactic option -> theory -> theory
    1.12 -  val add_inst_arity: xstring * string list * string -> string list
    1.13 +  val add_inst_subclass: xclass * xclass -> tactic -> theory -> theory
    1.14 +  val add_inst_subclass_i: class * class -> tactic -> theory -> theory
    1.15 +  val add_inst_arity_x: xstring * string list * string -> string list
    1.16      -> thm list -> tactic option -> theory -> theory
    1.17 -  val add_inst_arity_i: string * sort list * sort -> string list
    1.18 -    -> thm list -> tactic option -> theory -> theory
    1.19 +  val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
    1.20 +  val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
    1.21    val default_intro_classes_tac: thm list -> int -> tactic
    1.22    val axclass_tac: thm list -> tactic
    1.23    val prove_subclass: theory -> class * class -> thm list
    1.24 @@ -417,11 +417,15 @@
    1.25          prove_arity thy (t, Ss, c) wthms usr_tac);
    1.26    in add_arity_thms (map prove cs) thy end;
    1.27  
    1.28 +fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (Some tac);
    1.29 +fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (Some tac);
    1.30  
    1.31 -val add_inst_subclass = ext_inst_subclass read_classrel;
    1.32 -val add_inst_subclass_i = ext_inst_subclass cert_classrel;
    1.33 -val add_inst_arity = ext_inst_arity read_arity;
    1.34 -val add_inst_arity_i = ext_inst_arity cert_arity;
    1.35 +val add_inst_subclass_x = ext_inst_subclass read_classrel;
    1.36 +val add_inst_subclass = sane_inst_subclass read_classrel;
    1.37 +val add_inst_subclass_i = sane_inst_subclass cert_classrel;
    1.38 +val add_inst_arity_x = ext_inst_arity read_arity;
    1.39 +val add_inst_arity = sane_inst_arity read_arity;
    1.40 +val add_inst_arity_i = sane_inst_arity cert_arity;
    1.41  
    1.42  
    1.43  (* make old-style interactive goals *)