--- a/src/Pure/Isar/class.ML Mon Jul 06 19:58:52 2009 +0200
+++ b/src/Pure/Isar/class.ML Mon Jul 06 20:36:38 2009 +0200
@@ -90,7 +90,7 @@
val sup_of_classes = map (snd o rules thy) sups;
val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
val axclass_intro = #intro (AxClass.get_info thy class);
- val base_sort_trivs = Thm.sort_triv thy (aT, base_sort);
+ val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
val tac = REPEAT (SOMEGOAL
(Tactic.match_tac (axclass_intro :: sup_of_classes
@ loc_axiom_intros @ base_sort_trivs)
--- a/src/Pure/axclass.ML Mon Jul 06 19:58:52 2009 +0200
+++ b/src/Pure/axclass.ML Mon Jul 06 20:36:38 2009 +0200
@@ -214,7 +214,7 @@
|> snd))
end;
-fun complete_arities thy =
+fun complete_arities thy =
let
val arities = snd (get_instances thy);
val (completions, arities') = arities
@@ -575,12 +575,13 @@
fun derive_type _ (_, []) = []
| derive_type thy (typ, sort) =
let
+ val certT = Thm.ctyp_of thy;
val vars = Term.fold_atyps
(fn T as TFree (_, S) => insert (eq_fst op =) (T, S)
| T as TVar (_, S) => insert (eq_fst op =) (T, S)
| _ => I) typ [];
val hyps = vars
- |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
+ |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
val ths = (typ, sort)
|> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
{class_relation =
--- a/src/Pure/more_thm.ML Mon Jul 06 19:58:52 2009 +0200
+++ b/src/Pure/more_thm.ML Mon Jul 06 20:36:38 2009 +0200
@@ -26,7 +26,8 @@
val eq_thm_thy: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
val equiv_thm: thm * thm -> bool
- val sort_triv: theory -> typ * sort -> thm list
+ val class_triv: theory -> class -> thm
+ val of_sort: ctyp * sort -> thm list
val check_shyps: sort list -> thm -> thm
val is_dummy: thm -> bool
val plain_prop_of: thm -> term
@@ -171,14 +172,10 @@
(* type classes and sorts *)
-fun sort_triv thy (T, S) =
- let
- val certT = Thm.ctyp_of thy;
- val cT = certT T;
- fun class_triv c =
- Thm.class_triv thy c
- |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
- in map class_triv S end;
+fun class_triv thy c =
+ Thm.of_class (Thm.ctyp_of thy (TVar ((Name.aT, 0), [c])), c);
+
+fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
fun check_shyps sorts raw_th =
let
--- a/src/Pure/thm.ML Mon Jul 06 19:58:52 2009 +0200
+++ b/src/Pure/thm.ML Mon Jul 06 20:36:38 2009 +0200
@@ -92,7 +92,7 @@
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
val trivial: cterm -> thm
- val class_triv: theory -> class -> thm
+ val of_class: ctyp * class -> thm
val unconstrainT: ctyp -> thm -> thm
val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
@@ -1110,22 +1110,28 @@
tpairs = [],
prop = Logic.mk_implies (A, A)});
-(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
-fun class_triv thy raw_c =
+(*Axiom-scheme reflecting signature contents
+ T :: c
+ -------------------
+ OFCLASS(T, c_class)
+*)
+fun of_class (cT, raw_c) =
let
+ val Ctyp {thy_ref, T, ...} = cT;
+ val thy = Theory.deref thy_ref;
val c = Sign.certify_class thy raw_c;
- val T = TVar ((Name.aT, 0), [c]);
- val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c))
- handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
+ val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
in
- Thm (deriv_rule0 (Pt.OfClass (T, c)),
- {thy_ref = Theory.check_thy thy,
- tags = [],
- maxidx = maxidx,
- shyps = sorts,
- hyps = [],
- tpairs = [],
- prop = prop})
+ if Sign.of_sort thy (T, [c]) then
+ Thm (deriv_rule0 (Pt.OfClass (T, c)),
+ {thy_ref = Theory.check_thy thy,
+ tags = [],
+ maxidx = maxidx,
+ shyps = sorts,
+ hyps = [],
+ tpairs = [],
+ prop = prop})
+ else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
end;
(*Internalize sort constraints of type variable*)