--- a/src/HOL/Analysis/metric_arith.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML Mon Sep 06 14:05:22 2021 +0200
@@ -24,7 +24,7 @@
fun IF_UNSOLVED' tac i = IF_UNSOLVED (tac i)
fun REPEAT' tac i = REPEAT (tac i)
-fun free_in v ct = member (op aconvc) (Drule.cterm_frees_of ct) v
+fun free_in v ct = member (op aconvc) (Misc_Legacy.cterm_frees ct) v
(* build a cterm set with elements cts of type ty *)
fun mk_ct_set ctxt ty =
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Sep 06 14:05:22 2021 +0200
@@ -206,7 +206,7 @@
val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
val postcv = Simplifier.rewrite (put_simpset ss ctxt);
val nnf = K (nnf_conv ctxt then_conv postcv)
- val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_frees_of tm)
+ val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Misc_Legacy.cterm_frees tm)
(isolate_conv ctxt) nnf
(fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
whatis = whatis, simpset = ss}) vs
--- a/src/HOL/Decision_Procs/langford.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Mon Sep 06 14:05:22 2021 +0200
@@ -188,7 +188,7 @@
in
fn p =>
Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
- (Drule.cterm_frees_of p) (K Thm.reflexive) (K Thm.reflexive)
+ (Misc_Legacy.cterm_frees p) (K Thm.reflexive) (K Thm.reflexive)
(K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
end;
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Mon Sep 06 14:05:22 2021 +0200
@@ -868,10 +868,10 @@
then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
else raise Failure "substitutable_monomial"
| \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
- (substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg tm)))
+ (substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg tm)))
(Thm.dest_arg1 tm)
handle Failure _ =>
- substitutable_monomial (merge (op aconvc) (fvs, Drule.cterm_frees_of (Thm.dest_arg1 tm)))
+ substitutable_monomial (merge (op aconvc) (fvs, Misc_Legacy.cterm_frees (Thm.dest_arg1 tm)))
(Thm.dest_arg tm))
| _ => raise Failure "substitutable_monomial")
--- a/src/HOL/Tools/Qelim/qelim.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Mon Sep 06 14:05:22 2021 +0200
@@ -66,7 +66,7 @@
fun standard_qelim_conv ctxt atcv ncv qcv p =
let val pcv = pcv ctxt
- in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_frees_of p) atcv ncv qcv p end
+ in gen_qelim_conv ctxt pcv pcv pcv cons (Misc_Legacy.cterm_frees p) atcv ncv qcv p end
end;
--- a/src/HOL/Tools/groebner.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/HOL/Tools/groebner.ML Mon Sep 06 14:05:22 2021 +0200
@@ -528,7 +528,7 @@
fun simp_ex_conv ctxt =
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
-fun free_in v t = member op aconvc (Drule.cterm_frees_of t) v;
+fun free_in v t = member op aconvc (Misc_Legacy.cterm_frees t) v;
val vsubst = let
fun vsubst (t,v) tm =
@@ -736,7 +736,7 @@
val T = Thm.typ_of_cterm x;
val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
in Thm.apply all (Thm.lambda x p) end
- val avs = Drule.cterm_frees_of tm
+ val avs = Misc_Legacy.cterm_frees tm
val P' = fold mk_forall avs tm
val th1 = initial_conv ctxt (mk_neg P')
val (evs,bod) = strip_exists(concl th1) in
@@ -795,7 +795,7 @@
val mons = striplist(dest_binary ring_add_tm) t
in member (op aconvc) mons v andalso
forall (fn m => v aconvc m
- orelse not(member (op aconvc) (Drule.cterm_frees_of m) v)) mons
+ orelse not(member (op aconvc) (Misc_Legacy.cterm_frees m) v)) mons
end
fun isolate_variable vars tm =
@@ -850,7 +850,7 @@
fun isolate_monomials vars tm =
let
val (cmons,vmons) =
- List.partition (fn m => null (inter (op aconvc) vars (Drule.cterm_frees_of m)))
+ List.partition (fn m => null (inter (op aconvc) vars (Misc_Legacy.cterm_frees m)))
(striplist ring_dest_add tm)
val cofactors = map (fn v => find_multipliers v vmons) vars
val cnc = if null cmons then zero_tm
--- a/src/Pure/drule.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/Pure/drule.ML Mon Sep 06 14:05:22 2021 +0200
@@ -88,7 +88,6 @@
val mk_term: cterm -> thm
val dest_term: thm -> cterm
val cterm_rule: (thm -> thm) -> cterm -> cterm
- val cterm_frees_of: cterm -> cterm list
val dummy_thm: thm
val free_dummy_thm: thm
val is_sort_constraint: term -> bool
@@ -611,7 +610,6 @@
end;
fun cterm_rule f = dest_term o f o mk_term;
-val cterm_frees_of = Thm.frees_of o mk_term;
val dummy_thm = mk_term (certify Term.dummy_prop);
val free_dummy_thm = Thm.tag_free_dummy dummy_thm;
--- a/src/Pure/more_thm.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/Pure/more_thm.ML Mon Sep 06 14:05:22 2021 +0200
@@ -27,7 +27,6 @@
val aconvc: cterm * cterm -> bool
val add_tvars: thm -> ctyp Term_Subst.TVars.table -> ctyp Term_Subst.TVars.table
val add_vars: thm -> cterm Term_Subst.Vars.table -> cterm Term_Subst.Vars.table
- val frees_of: thm -> cterm list
val dest_funT: ctyp -> ctyp * ctyp
val strip_type: ctyp -> ctyp list * ctyp
val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -148,16 +147,6 @@
let val v = Term.dest_Var (Thm.term_of ct)
in tab |> not (Term_Subst.Vars.defined tab v) ? Term_Subst.Vars.update (v, ct) end);
-fun frees_of th =
- (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
- (fn ct => fn (set, list) =>
- let val v = Term.dest_Free (Thm.term_of ct) in
- if not (Term_Subst.Frees.defined set v)
- then (Term_Subst.Frees.add (v, ()) set, ct :: list)
- else (set, list)
- end)
- |> #2;
-
(* ctyp operations *)
--- a/src/Tools/misc_legacy.ML Mon Sep 06 13:49:36 2021 +0200
+++ b/src/Tools/misc_legacy.ML Mon Sep 06 14:05:22 2021 +0200
@@ -5,6 +5,8 @@
signature MISC_LEGACY =
sig
+ val thm_frees: thm -> cterm list
+ val cterm_frees: cterm -> cterm list
val add_term_names: term * string list -> string list
val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
val add_term_tfrees: term * (string * sort) list -> (string * sort) list
@@ -24,6 +26,18 @@
structure Misc_Legacy: MISC_LEGACY =
struct
+fun thm_frees th =
+ (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
+ (fn ct => fn (set, list) =>
+ let val v = Term.dest_Free (Thm.term_of ct) in
+ if not (Term_Subst.Frees.defined set v)
+ then (Term_Subst.Frees.add (v, ()) set, ct :: list)
+ else (set, list)
+ end)
+ |> #2;
+
+val cterm_frees = thm_frees o Drule.mk_term;
+
(*iterate a function over all types in a term*)
fun it_term_types f =
let fun iter(Const(_,T), a) = f(T,a)