# HG changeset patch
# User wenzelm
# Date 1303894179 -7200
# Node ID 39eefaef816a2ee426a588802b575b9842581a40
# Parent  42c7ef050bc36ef74f43195184729d27af1e591f
eliminated obsolete Function_Lib.frees_in_term;
simplified;

diff -r 42c7ef050bc3 -r 39eefaef816a src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed Apr 27 10:31:18 2011 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Apr 27 10:49:39 2011 +0200
@@ -451,10 +451,10 @@
     fun requantify orig_intro thm =
       let
         val (qs, t) = dest_all_all orig_intro
-        val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
-        val vars = Term.add_vars (prop_of thm) [] |> rev
+        val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T)
+        val vars = Term.add_vars (prop_of thm) []
         val varmap = AList.lookup (op =) (frees ~~ map fst vars)
-          #> the_default ("",0)
+          #> the_default ("", 0)
       in
         fold_rev (fn Free (n, T) =>
           forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
diff -r 42c7ef050bc3 -r 39eefaef816a src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 10:31:18 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Apr 27 10:49:39 2011 +0200
@@ -23,8 +23,6 @@
   val mk_forall_rename: (string * term) -> term -> term
   val forall_intr_rename: (string * cterm) -> thm -> thm
 
-  val frees_in_term: Proof.context -> term -> (string * typ) list
-
   datatype proof_attempt = Solved of thm | Stuck of thm | Fail
   val try_proof: cterm -> tactic -> proof_attempt
 
@@ -101,13 +99,6 @@
   end
 
 
-(* Returns the frees in a term in canonical order, excluding the fixes from the context *)
-fun frees_in_term ctxt t =
-  Term.add_frees t []
-  |> filter_out (Variable.is_fixed ctxt o fst)
-  |> rev
-
-
 datatype proof_attempt = Solved of thm | Stuck of thm | Fail
 
 fun try_proof cgoal tac =
diff -r 42c7ef050bc3 -r 39eefaef816a src/HOL/Tools/Function/pattern_split.ML
--- a/src/HOL/Tools/Function/pattern_split.ML	Wed Apr 27 10:31:18 2011 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML	Wed Apr 27 10:49:39 2011 +0200
@@ -86,9 +86,12 @@
     fun instantiate (vs', sigma) =
       let
         val t = Pattern.rewrite_term thy sigma [] feq1
-      in
-        fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctxt t))) t
-      end
+        val xs = fold_aterms
+          (fn x as Free (a, _) =>
+              if not (Variable.is_fixed ctxt a) andalso member (op =) vs' x
+              then insert (op =) x else I
+            | _ => I) t [];
+      in fold Logic.all xs t end
   in
     map instantiate substs
   end