# HG changeset patch
# User wenzelm
# Date 1213901283 -7200
# Node ID 39ff18c0f07fecc53a33567434fe08726e10624b
# Parent  1295745897344433ec9a458e68a4f99eff2a63ea
moved add_used to Isar/rule_insts.ML;

diff -r 129574589734 -r 39ff18c0f07f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Jun 19 20:48:02 2008 +0200
+++ b/src/Pure/drule.ML	Thu Jun 19 20:48:03 2008 +0200
@@ -78,7 +78,6 @@
   val strip_type: ctyp -> ctyp list * ctyp
   val beta_conv: cterm -> cterm -> cterm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
-  val add_used: thm -> string list -> string list
   val flexflex_unique: thm -> thm
   val store_thm: bstring -> thm -> thm
   val store_standard_thm: bstring -> thm -> thm
@@ -200,11 +199,6 @@
       if i < 0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a, i);
   in (types, sorts) end;
 
-val add_used =
-  (Thm.fold_terms o fold_types o fold_atyps)
-    (fn TFree (a, _) => insert (op =) a
-      | TVar ((a, _), _) => insert (op =) a
-      | _ => I);