renamed AxClass.get_definition to AxClass.get_info (again);
authorwenzelm
Tue Oct 09 17:10:41 2007 +0200 (2007-10-09 ago)
changeset 24929408becab067e
parent 24928 3419943838f5
child 24930 cc2e0e8c81af
renamed AxClass.get_definition to AxClass.get_info (again);
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Oct 09 17:10:38 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Oct 09 17:10:41 2007 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val add_arity: thm -> theory -> theory
     1.5    val prove_classrel: class * class -> tactic -> theory -> theory
     1.6    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
     1.7 -  val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list,
     1.8 +  val get_info: theory -> class -> {def: thm, intro: thm, axioms: thm list,
     1.9      params: (string * typ) list}
    1.10    val class_intros: theory -> thm list
    1.11    val class_of_param: theory -> string -> class option
    1.12 @@ -26,15 +26,15 @@
    1.13    val print_axclasses: theory -> unit
    1.14    val cert_classrel: theory -> class * class -> class * class
    1.15    val read_classrel: theory -> xstring * xstring -> class * class
    1.16 -  val axiomatize_class: bstring * xstring list -> theory -> theory
    1.17 -  val axiomatize_class_i: bstring * class list -> theory -> theory
    1.18 -  val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
    1.19 -  val axiomatize_classrel_i: (class * class) list -> theory -> theory
    1.20 -  val axiomatize_arity: xstring * string list * string -> theory -> theory
    1.21 -  val axiomatize_arity_i: arity -> theory -> theory
    1.22 +  val axiomatize_class: bstring * class list -> theory -> theory
    1.23 +  val axiomatize_class_cmd: bstring * xstring list -> theory -> theory
    1.24 +  val axiomatize_classrel: (class * class) list -> theory -> theory
    1.25 +  val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
    1.26 +  val axiomatize_arity: arity -> theory -> theory
    1.27 +  val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
    1.28    type cache
    1.29 +  val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
    1.30    val cache: cache
    1.31 -  val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
    1.32  end;
    1.33  
    1.34  structure AxClass: AX_CLASS =
    1.35 @@ -113,7 +113,7 @@
    1.36  
    1.37  val lookup_def = Symtab.lookup o #1 o get_axclasses;
    1.38  
    1.39 -fun get_definition thy c =
    1.40 +fun get_info thy c =
    1.41    (case lookup_def thy c of
    1.42      SOME (AxClass info) => info
    1.43    | NONE => error ("No such axclass: " ^ quote c));
    1.44 @@ -136,7 +136,7 @@
    1.45  fun class_of_param thy =
    1.46    AList.lookup (op =) (#2 (get_axclasses thy));
    1.47  
    1.48 -fun params_of_class thy class = (Name.aT, #params (get_definition thy class));
    1.49 +fun params_of_class thy class = (Name.aT, #params (get_info thy class));
    1.50  
    1.51  
    1.52  (* maintain instances *)
    1.53 @@ -156,7 +156,7 @@
    1.54  
    1.55  
    1.56  fun the_arity thy a (c, Ss) =
    1.57 -  (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss)  of
    1.58 +  (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
    1.59      SOME th => Thm.transfer thy th
    1.60    | NONE => error ("Unproven type arity " ^
    1.61        Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
    1.62 @@ -389,7 +389,7 @@
    1.63      |-> (fn cs => mk_axioms cs
    1.64      #-> (fn axioms_prop => define_class (name, superclasses)
    1.65             (map fst cs @ other_consts) axioms_prop
    1.66 -    #-> (fn class => `(fn thy => get_definition thy class)
    1.67 +    #-> (fn class => `(fn thy => get_info thy class)
    1.68      #-> (fn {axioms, ...} => fold (add_constraint class) cs
    1.69      #> pair (class, (cs, axioms))))))
    1.70    end;
    1.71 @@ -431,12 +431,12 @@
    1.72  
    1.73  in
    1.74  
    1.75 -val axiomatize_class = ax_class Sign.read_class read_classrel;
    1.76 -val axiomatize_class_i = ax_class Sign.certify_class cert_classrel;
    1.77 -val axiomatize_classrel = ax_classrel read_classrel;
    1.78 -val axiomatize_classrel_i = ax_classrel cert_classrel;
    1.79 -val axiomatize_arity = ax_arity Sign.read_arity;
    1.80 -val axiomatize_arity_i = ax_arity Sign.cert_arity;
    1.81 +val axiomatize_class = ax_class Sign.certify_class cert_classrel;
    1.82 +val axiomatize_class_cmd = ax_class Sign.read_class read_classrel;
    1.83 +val axiomatize_classrel = ax_classrel cert_classrel;
    1.84 +val axiomatize_classrel_cmd = ax_classrel read_classrel;
    1.85 +val axiomatize_arity = ax_arity Sign.cert_arity;
    1.86 +val axiomatize_arity_cmd = ax_arity Sign.read_arity;
    1.87  
    1.88  end;
    1.89  
    1.90 @@ -445,7 +445,6 @@
    1.91  (** explicit derivations -- cached **)
    1.92  
    1.93  datatype cache = Types of (class * thm) list Typtab.table;
    1.94 -val cache = Types Typtab.empty;
    1.95  
    1.96  local
    1.97  
    1.98 @@ -490,4 +489,6 @@
    1.99  
   1.100  end;
   1.101  
   1.102 +val cache = Types Typtab.empty;
   1.103 +
   1.104  end;