--- 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
--- 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 =
--- 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