diff -r 96abba46955f -r cb1966f3a92b src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Mar 19 22:31:23 2015 +0100
+++ b/src/Pure/drule.ML	Fri Mar 20 11:09:08 2015 +0100
@@ -58,7 +58,6 @@
   val strip_comb: cterm -> cterm * cterm list
   val strip_type: ctyp -> ctyp list * ctyp
   val beta_conv: cterm -> cterm -> cterm
-  val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val flexflex_unique: Proof.context option -> thm -> thm
   val export_without_context: thm -> thm
   val export_without_context_open: thm -> thm
@@ -172,27 +171,6 @@
 
 
 
-(*** Find the type (sort) associated with a (T)Var or (T)Free in a term
-     Used for establishing default types (of variables) and sorts (of
-     type variables) when reading another term.
-     Index -1 indicates that a (T)Free rather than a (T)Var is wanted.
-***)
-
-fun types_sorts thm =
-  let
-    val vars = Thm.fold_terms Term.add_vars thm [];
-    val frees = Thm.fold_terms Term.add_frees thm [];
-    val tvars = Thm.fold_terms Term.add_tvars thm [];
-    val tfrees = Thm.fold_terms Term.add_tfrees thm [];
-    fun types (a, i) =
-      if i < 0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a, i);
-    fun sorts (a, i) =
-      if i < 0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a, i);
-  in (types, sorts) end;
-
-
-
-
 (** Standardization of rules **)
 
 (*Generalization over a list of variables*)