--- 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;