# HG changeset patch
# User wenzelm
# Date 1246905398 -7200
# Node ID c8a35979a5bce44c84555d0790401429fceb6730
# Parent  5e960a0780a294d79b7e71a04016166fc9219dc2
clarified Thm.of_class/of_sort/class_triv;

diff -r 5e960a0780a2 -r c8a35979a5bc src/Pure/Isar/class.ML
--- 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)
diff -r 5e960a0780a2 -r c8a35979a5bc src/Pure/axclass.ML
--- 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 =
diff -r 5e960a0780a2 -r c8a35979a5bc src/Pure/more_thm.ML
--- 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
diff -r 5e960a0780a2 -r c8a35979a5bc src/Pure/thm.ML
--- 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*)