# HG changeset patch
# User wenzelm
# Date 1246562778 -7200
# Node ID a86896359ca4d6f60d3339474e28f3c7f7adc2fc
# Parent  c5221dbc40f6ed8f56b47e17dfd4e594d5c369b8
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);

diff -r c5221dbc40f6 -r a86896359ca4 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Jul 02 20:55:44 2009 +0200
+++ b/src/Pure/Isar/class.ML	Thu Jul 02 21:26:18 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 = Drule.sort_triv thy (aT, base_sort);
+    val base_sort_trivs = Thm.sort_triv thy (aT, base_sort);
     val tac = REPEAT (SOMEGOAL
       (Tactic.match_tac (axclass_intro :: sup_of_classes
          @ loc_axiom_intros @ base_sort_trivs)
diff -r c5221dbc40f6 -r a86896359ca4 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Jul 02 20:55:44 2009 +0200
+++ b/src/Pure/axclass.ML	Thu Jul 02 21:26:18 2009 +0200
@@ -580,7 +580,7 @@
               | T as TVar (_, S) => insert (eq_fst op =) (T, S)
               | _ => I) typ [];
         val hyps = vars
-          |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
+          |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
         val ths = (typ, sort)
           |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
            {class_relation =
diff -r c5221dbc40f6 -r a86896359ca4 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jul 02 20:55:44 2009 +0200
+++ b/src/Pure/drule.ML	Thu Jul 02 21:26:18 2009 +0200
@@ -108,7 +108,6 @@
   val dummy_thm: thm
   val sort_constraintI: thm
   val sort_constraint_eq: thm
-  val sort_triv: theory -> typ * sort -> thm list
   val unconstrainTs: thm -> thm
   val with_subgoal: int -> (thm -> thm) -> thm -> thm
   val comp_no_flatten: thm * int -> int -> thm -> thm
@@ -209,15 +208,6 @@
 
 (* 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 unconstrainTs th =
   fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
     (Thm.fold_terms Term.add_tvars th []) th;
diff -r c5221dbc40f6 -r a86896359ca4 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jul 02 20:55:44 2009 +0200
+++ b/src/Pure/more_thm.ML	Thu Jul 02 21:26:18 2009 +0200
@@ -26,6 +26,7 @@
   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 check_shyps: sort list -> thm -> thm
   val is_dummy: thm -> bool
   val plain_prop_of: thm -> term
@@ -168,7 +169,16 @@
   Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
 
 
-(* sort hypotheses *)
+(* 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 check_shyps sorts raw_th =
   let