# HG changeset patch
# User wenzelm
# Date 1131652642 -3600
# Node ID 1d1cc715a9e54edc91e54ea9dcda8c5194e75ae5
# Parent  32538cf750ca5079f352b184ce64bd2325028750
moved find_free to term.ML;

diff -r 32538cf750ca -r 1d1cc715a9e5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Nov 10 20:57:21 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 10 20:57:22 2005 +0100
@@ -66,7 +66,6 @@
   val read_const: context -> string -> term
   val warn_extra_tfrees: context -> context -> context
   val generalize: context -> context -> term list -> term list
-  val find_free: term -> string -> term option
   val export: context -> context -> thm -> thm
   val exports: context -> context -> thm -> thm Seq.seq
   val goal_exports: context -> context -> thm -> thm Seq.seq
@@ -708,11 +707,6 @@
 
 (** export theorems **)
 
-fun get_free x (t as Free (y, _)) NONE = if x = y then SOME t else NONE
-  | get_free _ _ opt = opt;
-
-fun find_free t x = fold_aterms (get_free x) t NONE;
-
 fun common_exports is_goal inner outer =
   let
     val gen = generalize_tfrees inner outer;
@@ -726,7 +720,7 @@
       let
         val thy = Thm.theory_of_thm rule;
         val prop = Thm.full_prop_of rule;
-        val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes);
+        val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes);
         val tfrees = gen (Term.add_term_tfree_names (prop, []));
       in
         rule