moved find_free to term.ML;
authorwenzelm
Thu Nov 10 20:57:22 2005 +0100 (2005-11-10)
changeset 181521d1cc715a9e5
parent 18151 32538cf750ca
child 18153 a084aa91f701
moved find_free to term.ML;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Nov 10 20:57:21 2005 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Nov 10 20:57:22 2005 +0100
     1.3 @@ -66,7 +66,6 @@
     1.4    val read_const: context -> string -> term
     1.5    val warn_extra_tfrees: context -> context -> context
     1.6    val generalize: context -> context -> term list -> term list
     1.7 -  val find_free: term -> string -> term option
     1.8    val export: context -> context -> thm -> thm
     1.9    val exports: context -> context -> thm -> thm Seq.seq
    1.10    val goal_exports: context -> context -> thm -> thm Seq.seq
    1.11 @@ -708,11 +707,6 @@
    1.12  
    1.13  (** export theorems **)
    1.14  
    1.15 -fun get_free x (t as Free (y, _)) NONE = if x = y then SOME t else NONE
    1.16 -  | get_free _ _ opt = opt;
    1.17 -
    1.18 -fun find_free t x = fold_aterms (get_free x) t NONE;
    1.19 -
    1.20  fun common_exports is_goal inner outer =
    1.21    let
    1.22      val gen = generalize_tfrees inner outer;
    1.23 @@ -726,7 +720,7 @@
    1.24        let
    1.25          val thy = Thm.theory_of_thm rule;
    1.26          val prop = Thm.full_prop_of rule;
    1.27 -        val frees = map (Thm.cterm_of thy) (List.mapPartial (find_free prop) fixes);
    1.28 +        val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes);
    1.29          val tfrees = gen (Term.add_term_tfree_names (prop, []));
    1.30        in
    1.31          rule