src/Pure/axclass.ML
changeset 3938 c20fbe3cb94f
parent 3854 762606a888fe
child 3949 c60ff6d0a6b8
     1.1 --- a/src/Pure/axclass.ML	Mon Oct 20 10:52:04 1997 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Oct 20 10:52:32 1997 +0200
     1.3 @@ -6,22 +6,22 @@
     1.4  *)
     1.5  
     1.6  signature AX_CLASS =
     1.7 -  sig
     1.8 +sig
     1.9    val add_thms_as_axms: (string * thm) list -> theory -> theory
    1.10    val add_classrel_thms: thm list -> theory -> theory
    1.11    val add_arity_thms: thm list -> theory -> theory
    1.12 -  val add_axclass: class * class list -> (string * string) list
    1.13 +  val add_axclass: rclass * xclass list -> (string * string) list
    1.14      -> theory -> theory
    1.15 -  val add_axclass_i: class * class list -> (string * term) list
    1.16 +  val add_axclass_i: rclass * class list -> (string * term) list
    1.17      -> theory -> theory
    1.18 +  val add_inst_subclass: xclass * xclass -> string list -> thm list
    1.19 +    -> tactic option -> theory -> theory
    1.20    val add_inst_subclass_i: class * class -> string list -> thm list
    1.21      -> tactic option -> theory -> theory
    1.22 -  val add_inst_subclass: class * class -> string list -> thm list
    1.23 -    -> tactic option -> theory -> theory
    1.24 +  val add_inst_arity: xstring * xsort list * xclass list -> string list
    1.25 +    -> thm list -> tactic option -> theory -> theory
    1.26    val add_inst_arity_i: string * sort list * class list -> string list
    1.27      -> thm list -> tactic option -> theory -> theory
    1.28 -  val add_inst_arity: string * sort list * class list -> string list
    1.29 -    -> thm list -> tactic option -> theory -> theory
    1.30    val axclass_tac: theory -> thm list -> tactic
    1.31    val prove_subclass: theory -> class * class -> thm list
    1.32      -> tactic option -> thm
    1.33 @@ -29,7 +29,7 @@
    1.34      -> tactic option -> thm
    1.35    val goal_subclass: theory -> class * class -> thm list
    1.36    val goal_arity: theory -> string * sort list * class -> thm list
    1.37 -  end;
    1.38 +end;
    1.39  
    1.40  structure AxClass : AX_CLASS =
    1.41  struct
    1.42 @@ -176,13 +176,17 @@
    1.43  
    1.44  fun ext_axclass int prep_axm (raw_class, raw_super_classes) raw_axioms old_thy =
    1.45    let
    1.46 -    val axioms = map (prep_axm (sign_of old_thy)) raw_axioms;
    1.47 +    val old_sign = sign_of old_thy;
    1.48 +    val axioms = map (prep_axm old_sign) raw_axioms;
    1.49 +    val class = Sign.full_name old_sign raw_class;
    1.50 +
    1.51      val thy =
    1.52        (if int then Theory.add_classes else Theory.add_classes_i)
    1.53          [(raw_class, raw_super_classes)] old_thy;
    1.54      val sign = sign_of thy;
    1.55 -    val class = Sign.intern_class sign raw_class;
    1.56 -    val super_classes = map (Sign.intern_class sign) raw_super_classes;
    1.57 +    val super_classes =
    1.58 +      if int then map (Sign.intern_class sign) raw_super_classes
    1.59 +      else raw_super_classes;
    1.60  
    1.61  
    1.62      (* prepare abstract axioms *)