renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.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)
--- 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 =
--- 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;
--- 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