--- a/src/Pure/Tools/class_package.ML Mon Feb 06 20:59:58 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Mon Feb 06 20:59:59 2006 +0100
@@ -246,7 +246,7 @@
fun gen_instance_arity prep_arity add_defs tap_def raw_arity raw_defs thy =
let
- val dest_def = Theory.dest_def (Sign.pp thy) handle TERM (msg, _) => error msg;
+ val pp = Sign.pp thy;
val arity as (tyco, asorts, sort) = prep_arity thy ((fn ((x, y), z) => (x, y, z)) raw_arity);
val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
fun get_c_req class =
@@ -268,7 +268,7 @@
fun check_defs raw_defs c_req thy =
let
val thy' = Sign.add_arities_i [(tyco, asorts, sort)] thy;
- val c_given = map (fst o dest_def o snd o tap_def thy' o fst) raw_defs;
+ val c_given = map (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_defs;
fun eq_c ((c1, ty1), (c2, ty2)) =
let
val ty1' = Type.varifyT ty1;
@@ -298,12 +298,6 @@
|-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
end;
-val _ : string option ->
- ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
- theory -> (term * (bstring * thm)) list * (Proof.context * theory)
- = Specification.definition_i;
-
-
val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x;
val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x;