--- a/src/HOL/Data_Structures/Define_Time_Function.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML Sat Nov 30 22:33:21 2024 +0100
@@ -883,7 +883,7 @@
| args _ = []
val dom_vars =
terms |> hd |> get_l |> map_types (map_atyps freeTypes)
- |> args |> Variable.variant_frees lthy []
+ |> args |> Variable.variant_names lthy
val dom_args =
List.foldl (fn (t,p) => HOLogic.mk_prod ((Free t),p)) (Free (hd dom_vars)) (tl dom_vars)
--- a/src/HOL/Hoare/hoare_tac.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Sat Nov 30 22:33:21 2024 +0100
@@ -87,7 +87,7 @@
fun Mset ctxt prop =
let
- val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())];
+ val [(Mset, _), (P, _)] = Variable.variant_names ctxt [("Mset", ()), ("P", ())];
val vars = get_vars prop;
val varsT = fastype_of (mk_bodyC vars);
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Nov 30 22:33:21 2024 +0100
@@ -274,11 +274,11 @@
in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
(* This assumes that distinct names are mapped to distinct names by
- "Variable.variant_frees". This does not hold in general but should hold for
+ "Variable.variant_names". This does not hold in general but should hold for
ATP-generated Skolem function names, since these end with a digit and
"variant_frees" appends letters. *)
fun desymbolize_and_fresh_up ctxt s =
- fst (hd (Variable.variant_frees ctxt [] [(Name.desymbolize (SOME false) s, ())]))
+ fst (singleton (Variable.variant_names ctxt) (Name.desymbolize (SOME false) s, ()))
(* Higher-order translation. Variables are typed (although we don't use that information). Lambdas
are typed. The code is similar to "term_of_atp_fo". *)
--- a/src/HOL/Tools/ATP/atp_util.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Sat Nov 30 22:33:21 2024 +0100
@@ -410,7 +410,7 @@
let
val (t, (frees, params)) =
Logic.goal_params (Thm.prop_of goal) i
- ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
+ ||> (map dest_Free #> Variable.variant_names ctxt #> `(map Free))
val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
in (rev params, hyp_ts, concl_t) end
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Nov 30 22:33:21 2024 +0100
@@ -262,7 +262,7 @@
|> mk_TFrees' (map Type.sort_of_atyp As0);
val fpT = Type (fpT_name, As);
- val (var_name, ()) = singleton (Variable.variant_frees ctxt []) ("x", ());
+ val (var_name, ()) = singleton (Variable.variant_names ctxt) ("x", ());
val var = Free (var_name, fpT);
val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var);
@@ -394,7 +394,7 @@
val fun_T = fastype_of fun_t;
val num_args = num_binder_types fun_T;
- val f = Free (singleton (Variable.variant_frees ctxt []) ("f", fun_T));
+ val f = Free (singleton (Variable.variant_names ctxt) ("f", fun_T));
val is_self_call = curry (op aconv) fun_t;
val has_self_call = exists_subterm is_self_call;
@@ -777,7 +777,8 @@
val (arg_Ts, _) = strip_type (fastype_of fun_t);
val added_Ts = drop (length arg_ts) arg_Ts;
val free_names = mk_names (length added_Ts) "x" ~~ added_Ts;
- val free_args = Variable.variant_frees ctxt [rhs, lhs] free_names |> map Free;
+ val free_args =
+ Variable.variant_names (fold Variable.declare_names [rhs, lhs] ctxt) free_names |> map Free;
in
(arg_ts @ free_args, list_comb (rhs, free_args))
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Nov 30 22:33:21 2024 +0100
@@ -1212,7 +1212,9 @@
(map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'');
val ps =
- Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
+ Variable.variant_names
+ (fold Variable.declare_names (maps (maps #fun_args) disc_eqnss) lthy)
+ [("P", HOLogic.boolT)];
val exhaust_thmss =
map2 (fn false => K []
--- a/src/HOL/Tools/Function/function_elims.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML Sat Nov 30 22:33:21 2024 +0100
@@ -79,7 +79,7 @@
val n_fs = length fs;
fun variant_free used_term v =
- Free (singleton (Variable.variant_frees ctxt [used_term]) v);
+ Free (singleton (Variable.variant_names (Variable.declare_names used_term ctxt)) v);
fun mk_partial_elim_rule (idx, f) =
let
--- a/src/HOL/Tools/Function/induction_schema.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Sat Nov 30 22:33:21 2024 +0100
@@ -121,7 +121,8 @@
val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
- val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
+ val (Pbool :: xs') =
+ map Free (Variable.variant_names (fold Variable.declare_names allqnames ctxt) (("P", HOLogic.boolT) :: xs))
val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
--- a/src/HOL/Tools/Function/mutual.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Sat Nov 30 22:33:21 2024 +0100
@@ -247,7 +247,7 @@
fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) =
let
val [P, x] =
- Variable.variant_frees ctxt [] [("P", \<^typ>\<open>bool\<close>), ("x", HOLogic.mk_tupleT Ts)]
+ Variable.variant_names ctxt [("P", \<^typ>\<open>bool\<close>), ("x", HOLogic.mk_tupleT Ts)]
|> map (Thm.cterm_of ctxt o Free);
val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x));
--- a/src/HOL/Tools/Function/pattern_split.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML Sat Nov 30 22:33:21 2024 +0100
@@ -20,7 +20,7 @@
fun new_var ctxt vs T =
let
- val [v] = Variable.variant_frees ctxt vs [("v", T)]
+ val v = singleton (Variable.variant_names (fold Variable.declare_names vs ctxt)) ("v", T)
in
(Free v :: vs, Free v)
end
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Nov 30 22:33:21 2024 +0100
@@ -991,8 +991,9 @@
mk_set_compr (t :: in_insert) ts xs
else
let
- val uu as (uuN, uuT) =
- singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
+ val uuT = fastype_of t
+ val uu as (uuN, _) =
+ singleton (Variable.variant_names (Variable.declare_names t ctxt')) ("uu", uuT)
val set_compr =
HOLogic.mk_Collect (uuN, uuT,
fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Nov 30 22:33:21 2024 +0100
@@ -1204,7 +1204,7 @@
fun define_quickcheck_predicate t thy =
let
val (vs, t') = strip_abs t
- val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *)
+ val vs' = Variable.variant_names (Proof_Context.init_global thy) vs (* FIXME proper context!? *)
val t'' = subst_bounds (map Free (rev vs'), t')
val (prems, concl) = strip_horn t''
val constname = "quickcheck"
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Nov 30 22:33:21 2024 +0100
@@ -279,14 +279,12 @@
let
val (constr, args) = strip_comb t
val T = fastype_of t
+ val ctxt1 = fold Variable.declare_names (concl :: assms) ctxt
val vars =
- map Free
- (Variable.variant_frees ctxt (concl :: assms)
- (map (fn t => ("x", fastype_of t)) args))
+ map Free (Variable.variant_names ctxt1 (map (fn t => ("x", fastype_of t)) args))
val varnames = map (fst o dest_Free) vars
- val dummy_var =
- Free (singleton
- (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
+ val ctxt2 = fold Variable.declare_names vars ctxt1
+ val dummy_var = Free (singleton (Variable.variant_names ctxt2) ("dummy", T))
val new_assms = map HOLogic.mk_eq (vars ~~ args)
val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Nov 30 22:33:21 2024 +0100
@@ -248,7 +248,7 @@
@{thm bot_fun_def}, @{thm less_bool_def}])
val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
val (vs, body) = strip_all t'
- val vs' = Variable.variant_frees ctxt [t'] vs
+ val vs' = Variable.variant_names (Variable.declare_names t' ctxt) vs
in subst_bounds (map Free (rev vs'), body) end
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Nov 30 22:33:21 2024 +0100
@@ -33,7 +33,7 @@
let
val [x, c] =
[("x", rty), ("c", HOLogic.mk_setT rty)]
- |> Variable.variant_frees lthy [rel]
+ |> Variable.variant_names (Variable.declare_names rel lthy)
|> map Free
in
HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Nov 30 22:33:21 2024 +0100
@@ -139,8 +139,8 @@
(cf. "~~/src/Pure/Isar/obtain.ML") *)
let
val frees = map Free xs
- val thesis =
- Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT))
+ val ctxt' = fold Variable.declare_names frees ctxt
+ val thesis = Free (singleton (Variable.variant_names ctxt') ("thesis", HOLogic.boolT))
val thesis_prop = HOLogic.mk_Trueprop thesis
(* !!x1...xn. t ==> thesis *)
--- a/src/HOL/Tools/inductive.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/HOL/Tools/inductive.ML Sat Nov 30 22:33:21 2024 +0100
@@ -925,12 +925,12 @@
val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
val fp_const = if coind then \<^Const>\<open>gfp predT\<close> else \<^Const>\<open>lfp predT\<close>;
+ val ctxt1 = fold Variable.declare_names intr_ts lthy
val p :: xs =
- map Free (Variable.variant_frees lthy intr_ts
+ map Free (Variable.variant_names ctxt1
(("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
- val bs =
- map Free (Variable.variant_frees lthy (p :: xs @ intr_ts)
- (map (rpair HOLogic.boolT) (mk_names "b" k)));
+ val ctxt2 = fold Variable.declare_names (p :: xs) ctxt1
+ val bs = map Free (Variable.variant_names ctxt2 (map (rpair HOLogic.boolT) (mk_names "b" k)));
fun subst t =
(case dest_predicate cs params t of
@@ -1001,8 +1001,8 @@
map_index (fn (i, ((b, mx), c)) =>
let
val Ts = arg_types_of (length params) c;
- val xs =
- map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts));
+ val ctxt = fold Variable.declare_names intr_ts lthy';
+ val xs = map Free (Variable.variant_names ctxt (mk_names "x" (length Ts) ~~ Ts));
in
((b, mx),
((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs)
--- a/src/Pure/Isar/object_logic.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/Pure/Isar/object_logic.ML Sat Nov 30 22:33:21 2024 +0100
@@ -159,7 +159,7 @@
fun is_propositional ctxt T =
T = propT orelse
- let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T))
+ let val x = Free (singleton (Variable.variant_names ctxt) ("x", T))
in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end;
--- a/src/Pure/variable.ML Sat Nov 30 22:02:36 2024 +0100
+++ b/src/Pure/variable.ML Sat Nov 30 22:33:21 2024 +0100
@@ -17,13 +17,13 @@
val def_sort: Proof.context -> indexname -> sort option
val declare_maxidx: int -> Proof.context -> Proof.context
val declare_names: term -> Proof.context -> Proof.context
+ val variant_names: Proof.context -> (string * 'a) list -> (string * 'a) list
val declare_constraints: term -> Proof.context -> Proof.context
val declare_internal: term -> Proof.context -> Proof.context
val declare_term: term -> Proof.context -> Proof.context
val declare_typ: typ -> Proof.context -> Proof.context
val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
val declare_thm: thm -> Proof.context -> Proof.context
- val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
val bind_term: indexname * term -> Proof.context -> Proof.context
val unbind_term: indexname -> Proof.context -> Proof.context
val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
@@ -211,7 +211,7 @@
val declare_maxidx = map_maxidx o Integer.max;
-(* names *)
+(* type/term names *)
fun declare_type_names t =
map_names (Term.declare_tfree_names t) #>
@@ -222,6 +222,8 @@
map_names (Term.declare_free_names t) #>
map_maxidx (Term.maxidx_term t);
+fun variant_names ctxt xs = Name.variant_names (names_of ctxt) xs;
+
(* type occurrences *)
@@ -275,12 +277,6 @@
val declare_thm = Thm.fold_terms {hyps = true} declare_internal;
-(* renaming term/type frees *)
-
-fun variant_frees ctxt ts frees =
- Name.variant_names (names_of (fold declare_names ts ctxt)) frees;
-
-
(** term bindings **)