# HG changeset patch # User wenzelm # Date 1733516827 -3600 # Node ID 692241432a995713511e136b0cfb50fad1524518 # Parent 41b387d477398579652844c92f1a98982e500ea6# Parent 7a1001f4c6004c9e99e1ba68f723d7f186c7a8f3 merged diff -r 41b387d47739 -r 692241432a99 NEWS --- a/NEWS Thu Dec 05 19:44:53 2024 +0100 +++ b/NEWS Fri Dec 06 21:27:07 2024 +0100 @@ -119,6 +119,10 @@ unbundle no datatype_record_syntax +* Printing of constants and bound variables is more careful to avoid +free variables, and fixed variables with mixfix syntax (including +'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac". + *** Isabelle/jEdit Prover IDE *** @@ -241,6 +245,17 @@ *** ML *** +* Term.variant_bounds replaces former Term.variant_frees for logical +manipulation of terms, without inner-syntax operations (e.g. reading a +term in the context of goal parameters). In contrast, former +Term.variant_frees made some attempts to work with constants as well, +but without taking the formal name space or abbreviations into account. +The existing operations Logic.goal_params, Logic.concl_of_goal, +Logic.prems_of_goal are now based on Term.variant_bounds, and thus +change their semantics silently! Rare INCOMPATIBILITY, better use +Variable.variant_names or Variable.focus_params, instead of +Logic.goal_params etc. + * Antiquotation \<^bundle>\name\ inlines a formally checked bundle name. * The new operation Pattern.rewrite_term_yoyo alternates top-down, diff -r 41b387d47739 -r 692241432a99 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/FOL/IFOL.thy Fri Dec 06 21:27:07 2024 +0100 @@ -105,7 +105,7 @@ syntax_consts "_Uniq" \ Uniq translations "\\<^sub>\\<^sub>1x. P" \ "CONST Uniq (\x. P)" typed_print_translation \ - [(\<^const_syntax>\Uniq\, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\_Uniq\)] + [(\<^const_syntax>\Uniq\, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\_Uniq\)] \ \ \to avoid eta-contraction of body\ diff -r 41b387d47739 -r 692241432a99 src/HOL/Auth/Guard/Proto.thy --- a/src/HOL/Auth/Guard/Proto.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Auth/Guard/Proto.thy Fri Dec 06 21:27:07 2024 +0100 @@ -464,7 +464,7 @@ apply (frule Guard_safe, simp) apply (frule Crypt_guard_invKey, simp) apply (frule ok_Guard, simp, simp, simp, clarsimp) -apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp) +apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp) apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+) apply (simp add: secret_def, simp add: secret_def, force, force) apply (simp add: secret_def keys_def, blast) @@ -475,7 +475,7 @@ apply (frule Guard_safe, simp) apply (frule Crypt_guard_invKey, simp) apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp) -apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp) +apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp) apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+) apply (simp add: secret_def, simp add: secret_def, force, force) apply (simp add: secret_def, rule No_Nonce, simp) @@ -493,7 +493,7 @@ apply (frule Guard_safe, simp) apply (frule Crypt_guard_invKey, simp) apply (frule ok_Guard, simp, simp, simp, clarsimp) -apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp) +apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp) apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+) apply (simp add: secret_def, simp add: secret_def, force, force) apply (simp add: secret_def, rule No_Nonce, simp) @@ -503,7 +503,7 @@ apply (frule Guard_safe, simp) apply (frule Crypt_guard_invKey, simp) apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp) -apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp) +apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp) apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+) apply (simp add: secret_def, simp add: secret_def, force, force) apply (simp add: secret_def keys_def, blast) diff -r 41b387d47739 -r 692241432a99 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/HOL.thy Fri Dec 06 21:27:07 2024 +0100 @@ -135,7 +135,7 @@ translations "\\<^sub>\\<^sub>1x. P" \ "CONST Uniq (\x. P)" typed_print_translation \ - [(\<^const_syntax>\Uniq\, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\_Uniq\)] + [(\<^const_syntax>\Uniq\, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\_Uniq\)] \ \ \to avoid eta-contraction of body\ @@ -150,7 +150,7 @@ translations "\!x. P" \ "CONST Ex1 (\x. P)" typed_print_translation \ - [(\<^const_syntax>\Ex1\, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\_Ex1\)] + [(\<^const_syntax>\Ex1\, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\_Ex1\)] \ \ \to avoid eta-contraction of body\ @@ -183,8 +183,8 @@ syntax_consts "_The" \ The translations "THE x. P" \ "CONST The (\x. P)" print_translation \ - [(\<^const_syntax>\The\, fn _ => fn [Abs abs] => - let val (x, t) = Syntax_Trans.atomic_abs_tr' abs + [(\<^const_syntax>\The\, fn ctxt => fn [Abs abs] => + let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs in Syntax.const \<^syntax_const>\_The\ $ x $ t end)] \ \ \To avoid eta-contraction of body\ diff -r 41b387d47739 -r 692241432a99 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/HOLCF/Cfun.thy Fri Dec 06 21:27:07 2024 +0100 @@ -39,8 +39,8 @@ \ print_translation \ - [(\<^const_syntax>\Abs_cfun\, fn _ => fn [Abs abs] => - let val (x, t) = Syntax_Trans.atomic_abs_tr' abs + [(\<^const_syntax>\Abs_cfun\, fn ctxt => fn [Abs abs] => + let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs in Syntax.const \<^syntax_const>\_cabs\ $ x $ t end)] \ \ \To avoid eta-contraction of body\ diff -r 41b387d47739 -r 692241432a99 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Dec 06 21:27:07 2024 +0100 @@ -142,29 +142,29 @@ print_translation \ let - fun dest_LAM (Const (\<^const_syntax>\Rep_cfun\,_) $ Const (\<^const_syntax>\unit_when\,_) $ t) = + fun dest_LAM _ (Const (\<^const_syntax>\Rep_cfun\,_) $ Const (\<^const_syntax>\unit_when\,_) $ t) = (Syntax.const \<^syntax_const>\_noargs\, t) - | dest_LAM (Const (\<^const_syntax>\Rep_cfun\,_) $ Const (\<^const_syntax>\csplit\,_) $ t) = + | dest_LAM ctxt (Const (\<^const_syntax>\Rep_cfun\,_) $ Const (\<^const_syntax>\csplit\,_) $ t) = let - val (v1, t1) = dest_LAM t; - val (v2, t2) = dest_LAM t1; + val (v1, t1) = dest_LAM ctxt t; + val (v2, t2) = dest_LAM ctxt t1; in (Syntax.const \<^syntax_const>\_args\ $ v1 $ v2, t2) end - | dest_LAM (Const (\<^const_syntax>\Abs_cfun\,_) $ t) = + | dest_LAM ctxt (Const (\<^const_syntax>\Abs_cfun\,_) $ t) = let val abs = case t of Abs abs => abs | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); - val (x, t') = Syntax_Trans.atomic_abs_tr' abs; + val (x, t') = Syntax_Trans.atomic_abs_tr' ctxt abs; in (Syntax.const \<^syntax_const>\_variable\ $ x, t') end - | dest_LAM _ = raise Match; (* too few vars: abort translation *) + | dest_LAM _ _ = raise Match; (* too few vars: abort translation *) - fun Case1_tr' [Const(\<^const_syntax>\branch\,_) $ p, r] = - let val (v, t) = dest_LAM r in + fun Case1_tr' ctxt [Const(\<^const_syntax>\branch\,_) $ p, r] = + let val (v, t) = dest_LAM ctxt r in Syntax.const \<^syntax_const>\_Case1\ $ (Syntax.const \<^syntax_const>\_match\ $ p $ v) $ t end; - in [(\<^const_syntax>\Rep_cfun\, K Case1_tr')] end + in [(\<^const_syntax>\Rep_cfun\, Case1_tr')] end \ translations diff -r 41b387d47739 -r 692241432a99 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Hilbert_Choice.thy Fri Dec 06 21:27:07 2024 +0100 @@ -29,8 +29,8 @@ "SOME x. P" \ "CONST Eps (\x. P)" print_translation \ - [(\<^const_syntax>\Eps\, fn _ => fn [Abs abs] => - let val (x, t) = Syntax_Trans.atomic_abs_tr' abs + [(\<^const_syntax>\Eps\, fn ctxt => fn [Abs abs] => + let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs in Syntax.const \<^syntax_const>\_Eps\ $ x $ t end)] \ \ \to avoid eta-contraction of body\ diff -r 41b387d47739 -r 692241432a99 src/HOL/Hoare_Parallel/RG_Examples.thy --- a/src/HOL/Hoare_Parallel/RG_Examples.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Fri Dec 06 21:27:07 2024 +0100 @@ -117,11 +117,11 @@ apply simp apply clarify apply simp - apply(subgoal_tac "xa=0") + apply(subgoal_tac "x=0") apply simp apply arith apply clarify - apply(case_tac xaa, simp, simp) + apply(case_tac xa, simp, simp) apply clarify apply simp apply(erule_tac x=0 in all_dupE) diff -r 41b387d47739 -r 692241432a99 src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Library/FSet.thy Fri Dec 06 21:27:07 2024 +0100 @@ -216,8 +216,8 @@ "\!x|\|A. P" \ "\!x. x |\| A \ P" typed_print_translation \ - [(\<^const_syntax>\fBall\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBall\), - (\<^const_syntax>\fBex\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBex\)] + [(\<^const_syntax>\fBall\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBall\), + (\<^const_syntax>\fBex\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_fBex\)] \ \ \to avoid eta-contraction of body\ syntax diff -r 41b387d47739 -r 692241432a99 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Library/Multiset.thy Fri Dec 06 21:27:07 2024 +0100 @@ -181,8 +181,8 @@ "\x\#A. P" \ "CONST Multiset.Bex A (\x. P)" typed_print_translation \ - [(\<^const_syntax>\Multiset.Ball\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_MBall\), - (\<^const_syntax>\Multiset.Bex\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_MBex\)] + [(\<^const_syntax>\Multiset.Ball\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_MBall\), + (\<^const_syntax>\Multiset.Bex\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_MBex\)] \ \ \to avoid eta-contraction of body\ lemma count_eq_zero_iff: diff -r 41b387d47739 -r 692241432a99 src/HOL/Library/conditional_parametricity.ML --- a/src/HOL/Library/conditional_parametricity.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Library/conditional_parametricity.ML Fri Dec 06 21:27:07 2024 +0100 @@ -246,7 +246,7 @@ val i = maxidx_of_term t + 1; fun tvar_to_tfree ((name, _), sort) = (name, sort); val tvars = Term.add_tvars t []; - val new_frees = map TFree (Term.variant_frees t (map tvar_to_tfree tvars)); + val new_frees = map TFree (Term.variant_bounds t (map tvar_to_tfree tvars)); val u = subst_atomic_types ((map TVar tvars) ~~ new_frees) t; val T = fastype_of t; val U = fastype_of u; diff -r 41b387d47739 -r 692241432a99 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Library/refute.ML Fri Dec 06 21:27:07 2024 +0100 @@ -1186,7 +1186,7 @@ (a, T) :: strip_all_vars t | strip_all_vars _ = [] : (string * typ) list val strip_t = strip_all_body ex_closure - val frees = Term.variant_frees strip_t (strip_all_vars ex_closure) + val frees = Term.variant_bounds strip_t (strip_all_vars ex_closure) val subst_t = Term.subst_bounds (map Free (rev frees), strip_t) in find_model ctxt (actual_params ctxt params) assm_ts subst_t true diff -r 41b387d47739 -r 692241432a99 src/HOL/Nominal/Examples/Class2.thy --- a/src/HOL/Nominal/Examples/Class2.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Nominal/Examples/Class2.thy Fri Dec 06 21:27:07 2024 +0100 @@ -4671,7 +4671,7 @@ apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] -apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) @@ -4679,17 +4679,17 @@ apply(auto intro: CANDs_alpha)[1] apply(case_tac "x=ya") apply(simp) -apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) apply(case_tac "za=ya") apply(simp) -apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) -apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(case_tac "x=xa") @@ -4707,7 +4707,7 @@ apply(drule_tac pi="[(x,za)]" and x="(xa):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] -apply(drule_tac pi="[(x,za)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,za)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(case_tac "x=xa") @@ -4727,17 +4727,17 @@ apply(auto intro: CANDs_alpha)[1] apply(case_tac "x=ya") apply(simp) -apply(drule_tac pi="[(ya,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(ya,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) apply(case_tac "za=ya") apply(simp) -apply(drule_tac pi="[(x,ya)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,ya)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) -apply(drule_tac pi="[(x,za)]" and x="(ya):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,za)]" and x="(ya):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] done @@ -4800,7 +4800,7 @@ apply(drule_tac pi="[(x,y)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] -apply(drule_tac pi="[(x,y)]" and x="(x):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,y)]" and x="(x):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(drule_tac pi="[(x,y)]" and x=":Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) @@ -4808,17 +4808,17 @@ apply(auto intro: CANDs_alpha)[1] apply(case_tac "x=xa") apply(simp) -apply(drule_tac pi="[(xa,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(xa,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) apply(case_tac "y=xa") apply(simp) -apply(drule_tac pi="[(x,xa)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,xa)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] apply(simp) -apply(drule_tac pi="[(x,y)]" and x="(xa):Nb" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) +apply(drule_tac pi="[(x,y)]" and x="(xa):Na" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: CAND_eqvt_name calc_atm) apply(auto intro: CANDs_alpha)[1] done diff -r 41b387d47739 -r 692241432a99 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Dec 06 21:27:07 2024 +0100 @@ -245,7 +245,7 @@ if null (preds_of ps prem) then prem else lift_prem prem) prems, HOLogic.mk_Trueprop (lift_pred p ts)); - val vs = map (Var o apfst (rpair 0)) (Term.variant_frees prem params') + val vs = map (Var o apfst (rpair 0)) (Term.variant_bounds prem params') in (Logic.list_all (params', prem), (vs, subst_bounds (rev vs, prem))) end) prems); diff -r 41b387d47739 -r 692241432a99 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Dec 06 21:27:07 2024 +0100 @@ -146,7 +146,7 @@ in Option.map prove (map_term f prop (the_default prop opt)) end; fun abs_params params t = - let val vs = map (Var o apfst (rpair 0)) (Term.variant_frees t params) + let val vs = map (Var o apfst (rpair 0)) (Term.variant_bounds t params) in (Logic.list_all (params, t), (vs, subst_bounds (rev vs, t))) end; fun inst_params thy (vs, p) th cts = diff -r 41b387d47739 -r 692241432a99 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Dec 06 21:27:07 2024 +0100 @@ -156,7 +156,7 @@ let val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); val rargs = map (rpair dummyT o fst o fst) recs; - val subs = Term.variant_frees rhs rargs; + val subs = Term.variant_bounds rhs rargs; val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => (Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss') handle RecError s => primrec_eq_err lthy s eq diff -r 41b387d47739 -r 692241432a99 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Fri Dec 06 21:27:07 2024 +0100 @@ -283,7 +283,7 @@ end | unnest_tuples pat = pat - fun tr' [sig_alg, Const (\<^const_syntax>\Collect\, _) $ t] = + fun tr' ctxt [sig_alg, Const (\<^const_syntax>\Collect\, _) $ t] = let val bound_dummyT = Const (\<^syntax_const>\_bound\, dummyT) @@ -300,7 +300,7 @@ end | go pattern elem (Abs abs) = let - val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs + val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' ctxt abs in go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t end @@ -313,7 +313,7 @@ go [] [] t end in - [(\<^const_syntax>\Sigma_Algebra.measure\, K tr')] + [(\<^const_syntax>\Sigma_Algebra.measure\, tr')] end \ diff -r 41b387d47739 -r 692241432a99 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Product_Type.thy Fri Dec 06 21:27:07 2024 +0100 @@ -315,34 +315,34 @@ typed_print_translation \ let - fun case_prod_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match - | case_prod_guess_names_tr' T [Abs (x, xT, t)] = + fun case_prod_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match + | case_prod_guess_names_tr' ctxt T [Abs (x, xT, t)] = (case (head_of t) of Const (\<^const_syntax>\case_prod\, _) => raise Match | _ => let val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; - val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); - val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t'); + val (y, t') = Syntax_Trans.atomic_abs_tr' ctxt ("y", yT, incr_boundvars 1 t $ Bound 0); + val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, xT, t'); in Syntax.const \<^syntax_const>\_abs\ $ (Syntax.const \<^syntax_const>\_pattern\ $ x' $ y) $ t'' end) - | case_prod_guess_names_tr' T [t] = + | case_prod_guess_names_tr' ctxt T [t] = (case head_of t of Const (\<^const_syntax>\case_prod\, _) => raise Match | _ => let val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; val (y, t') = - Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); - val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t'); + Syntax_Trans.atomic_abs_tr' ctxt ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); + val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt ("x", xT, t'); in Syntax.const \<^syntax_const>\_abs\ $ (Syntax.const \<^syntax_const>\_pattern\ $ x' $ y) $ t'' end) - | case_prod_guess_names_tr' _ _ = raise Match; - in [(\<^const_syntax>\case_prod\, K case_prod_guess_names_tr')] end + | case_prod_guess_names_tr' _ _ _ = raise Match; + in [(\<^const_syntax>\case_prod\, case_prod_guess_names_tr')] end \ text \Reconstruct pattern from (nested) \<^const>\case_prod\s, @@ -351,39 +351,39 @@ print_translation \ let - fun case_prod_tr' [Abs (x, T, t as (Abs abs))] = + fun case_prod_tr' ctxt [Abs (x, T, t as (Abs abs))] = (* case_prod (\x y. t) \ \(x, y) t *) let - val (y, t') = Syntax_Trans.atomic_abs_tr' abs; - val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); + val (y, t') = Syntax_Trans.atomic_abs_tr' ctxt abs; + val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, t'); in Syntax.const \<^syntax_const>\_abs\ $ (Syntax.const \<^syntax_const>\_pattern\ $ x' $ y) $ t'' end - | case_prod_tr' [Abs (x, T, (s as Const (\<^const_syntax>\case_prod\, _) $ t))] = + | case_prod_tr' ctxt [Abs (x, T, (s as Const (\<^const_syntax>\case_prod\, _) $ t))] = (* case_prod (\x. (case_prod (\y z. t))) \ \(x, y, z). t *) let val Const (\<^syntax_const>\_abs\, _) $ (Const (\<^syntax_const>\_pattern\, _) $ y $ z) $ t' = - case_prod_tr' [t]; - val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); + case_prod_tr' ctxt [t]; + val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, t'); in Syntax.const \<^syntax_const>\_abs\ $ (Syntax.const \<^syntax_const>\_pattern\ $ x' $ (Syntax.const \<^syntax_const>\_patterns\ $ y $ z)) $ t'' end - | case_prod_tr' [Const (\<^const_syntax>\case_prod\, _) $ t] = + | case_prod_tr' ctxt [Const (\<^const_syntax>\case_prod\, _) $ t] = (* case_prod (case_prod (\x y z. t)) \ \((x, y), z). t *) - case_prod_tr' [(case_prod_tr' [t])] + case_prod_tr' ctxt [(case_prod_tr' ctxt [t])] (* inner case_prod_tr' creates next pattern *) - | case_prod_tr' [Const (\<^syntax_const>\_abs\, _) $ x_y $ Abs abs] = + | case_prod_tr' ctxt [Const (\<^syntax_const>\_abs\, _) $ x_y $ Abs abs] = (* case_prod (\pttrn z. t) \ \(pttrn, z). t *) - let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in + let val (z, t) = Syntax_Trans.atomic_abs_tr' ctxt abs in Syntax.const \<^syntax_const>\_abs\ $ (Syntax.const \<^syntax_const>\_pattern\ $ x_y $ z) $ t end - | case_prod_tr' _ = raise Match; - in [(\<^const_syntax>\case_prod\, K case_prod_tr')] end + | case_prod_tr' _ _ = raise Match; + in [(\<^const_syntax>\case_prod\, case_prod_tr')] end \ diff -r 41b387d47739 -r 692241432a99 src/HOL/Set.thy --- a/src/HOL/Set.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Set.thy Fri Dec 06 21:27:07 2024 +0100 @@ -324,8 +324,8 @@ \ typed_print_translation \ - [(\<^const_syntax>\Ball\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_Ball\), - (\<^const_syntax>\Bex\, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_Bex\)] + [(\<^const_syntax>\Ball\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_Ball\), + (\<^const_syntax>\Bex\, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\_Bex\)] \ \ \to avoid eta-contraction of body\ print_translation \ @@ -348,7 +348,7 @@ if check (P, 0) then tr' P else let - val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs; + val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs; val M = Syntax.const \<^syntax_const>\_Coll\ $ x $ t; in case t of diff -r 41b387d47739 -r 692241432a99 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Dec 06 21:27:07 2024 +0100 @@ -391,10 +391,10 @@ |> map_filter (try (apsnd (fn Nested_Rec p => p))); fun ensure_unique frees t = - if member (op =) frees t then Free (the_single (Term.variant_frees t [dest_Free t])) else t; + if member (op =) frees t then Free (the_single (Term.variant_bounds t [dest_Free t])) else t; val args = replicate n_args ("", dummyT) - |> Term.variant_frees t + |> Term.variant_bounds t |> rev |> map Free |> fold (fn (ctr_arg_idx, (arg_idx, _)) => diff -r 41b387d47739 -r 692241432a99 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Dec 06 21:27:07 2024 +0100 @@ -477,7 +477,7 @@ map (pair "x") (drop j (take i (binder_types (fastype_of t)))), []) else chop i zs; val u = fold_rev Term.abs ys (strip_abs_body t); - val xs' = map Free (Name.variant_names (Term.declare_term_names u used) xs); + val xs' = map Free (Name.variant_names (Term.declare_free_names u used) xs); val (xs1, xs2) = chop j xs' in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end; fun is_dependent i t = diff -r 41b387d47739 -r 692241432a99 src/HOL/Tools/Old_Datatype/old_primrec.ML --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Fri Dec 06 21:27:07 2024 +0100 @@ -149,7 +149,7 @@ let val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs); val rargs = map (rpair dummyT o fst o fst) recs; - val subs = Term.variant_frees rhs rargs; + val subs = Term.variant_bounds rhs rargs; val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z => (Free x, (Old_Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss') handle PrimrecError (s, NONE) => primrec_error_eqn s eq diff -r 41b387d47739 -r 692241432a99 src/Provers/preorder.ML --- a/src/Provers/preorder.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Provers/preorder.ML Fri Dec 06 21:27:07 2024 +0100 @@ -555,7 +555,7 @@ fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st => let val thy = Proof_Context.theory_of ctxt; - val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A))); + val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A))); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); val lesss = flat (map_index (mkasm_trans thy o swap) Hs); @@ -578,7 +578,7 @@ fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st => let val thy = Proof_Context.theory_of ctxt - val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A))); + val rfrees = map Free (rev (Term.variant_bounds A (Logic.strip_params A))); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); val lesss = flat (map_index (mkasm_quasi thy o swap) Hs); diff -r 41b387d47739 -r 692241432a99 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/General/name_space.ML Fri Dec 06 21:27:07 2024 +0100 @@ -28,7 +28,7 @@ val names_long: bool Config.T val names_short: bool Config.T val names_unique: bool Config.T - val extern_generic: Context.generic -> T -> string -> xstring + val extern_if: (xstring -> bool) -> Proof.context -> T -> string -> xstring val extern: Proof.context -> T -> string -> xstring val extern_ord: Proof.context -> T -> string ord val extern_shortest: Proof.context -> T -> string -> xstring @@ -292,16 +292,17 @@ val names_short = Config.declare_option_bool ("names_short", \<^here>); val names_unique = Config.declare_option_bool ("names_unique", \<^here>); -fun extern_generic context space name = +fun extern_if ok ctxt space name = let - val names_long = Config.get_generic context names_long; - val names_short = Config.get_generic context names_short; - val names_unique = Config.get_generic context names_unique; + val names_long = Config.get ctxt names_long; + val names_short = Config.get ctxt names_short; + val names_unique = Config.get ctxt names_unique; fun extern_chunks require_unique a chunks = let val {full_name = c, unique, ...} = intern_chunks space chunks in - if (not require_unique orelse unique) andalso is_alias space c a - then SOME (Long_Name.implode_chunks chunks) + if (not require_unique orelse unique) andalso is_alias space c a then + let val x = Long_Name.implode_chunks chunks + in if ok x then SOME x else NONE end else NONE end; @@ -322,7 +323,7 @@ else extern_names (get_aliases space name) end; -val extern = extern_generic o Context.Proof; +val extern = extern_if (K true); fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space); diff -r 41b387d47739 -r 692241432a99 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/General/table.ML Fri Dec 06 21:27:07 2024 +0100 @@ -68,6 +68,7 @@ val make_set: key list -> set type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int} val unsynchronized_cache: (key -> 'a) -> 'a cache_ops + val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a end; functor Table(Key: KEY): TABLE = @@ -610,6 +611,8 @@ fun total_size () = size (! cache1) + size (! cache2); in {apply = apply, reset = reset, size = total_size} end; +fun apply_unsynchronized_cache f = #apply (unsynchronized_cache f); + (* ML pretty-printing *) diff -r 41b387d47739 -r 692241432a99 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Isar/expression.ML Fri Dec 06 21:27:07 2024 +0100 @@ -66,7 +66,7 @@ (** Internalise locale names in expr **) -fun check_expr thy instances = map (apfst (Locale.check thy)) instances; +fun check_expr ctxt instances = map (apfst (Locale.check ctxt)) instances; (** Parameters of expression **) @@ -378,7 +378,7 @@ let val thy = Proof_Context.theory_of ctxt1; - val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); + val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr ctxt1) raw_import); fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let diff -r 41b387d47739 -r 692241432a99 src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Isar/interpretation.ML Fri Dec 06 21:27:07 2024 +0100 @@ -215,7 +215,7 @@ gen_global_sublocale (K I) cert_interpretation expression; fun global_sublocale_cmd raw_expression = - gen_global_sublocale Locale.check read_interpretation raw_expression; + gen_global_sublocale Locale.check_global read_interpretation raw_expression; end; diff -r 41b387d47739 -r 692241432a99 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Isar/locale.ML Fri Dec 06 21:27:07 2024 +0100 @@ -44,8 +44,9 @@ (string * morphism) list -> theory -> theory val locale_space: theory -> Name_Space.T val intern: theory -> xstring -> string - val check: theory -> xstring * Position.T -> string - val extern: theory -> string -> xstring + val check_global: theory -> xstring * Position.T -> string + val check: Proof.context -> xstring * Position.T -> string + val extern: Proof.context -> string -> xstring val markup_name: Proof.context -> string -> string val pretty_name: Proof.context -> string -> Pretty.T val defined: theory -> string -> bool @@ -192,15 +193,20 @@ val locale_space = Name_Space.space_of_table o Locales.get; val intern = Name_Space.intern o locale_space; -fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); + +fun check_global thy = + #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); + +fun check ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (Locales.get (Proof_Context.theory_of ctxt)); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\locale\ - (Args.theory -- Scan.lift Parse.embedded_position >> + (Args.context -- Scan.lift Parse.embedded_position >> (ML_Syntax.print_string o uncurry check))); -fun extern thy = - Name_Space.extern_generic (Context.Theory thy) (locale_space thy); +fun extern ctxt = + Name_Space.extern ctxt (locale_space (Proof_Context.theory_of ctxt)); fun markup_extern ctxt = Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt)); diff -r 41b387d47739 -r 692241432a99 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Dec 06 21:27:07 2024 +0100 @@ -42,6 +42,9 @@ val class_space: Proof.context -> Name_Space.T val type_space: Proof.context -> Name_Space.T val const_space: Proof.context -> Name_Space.T + val lookup_free: Proof.context -> string -> string option + val printable_const: Proof.context -> string -> bool + val exclude_consts: Symset.T -> Proof.context -> Proof.context val defs_context: Proof.context -> Defs.context val intern_class: Proof.context -> xstring -> string val intern_type: Proof.context -> xstring -> string @@ -53,6 +56,8 @@ val markup_type: Proof.context -> string -> string val pretty_type: Proof.context -> string -> Pretty.T val extern_const: Proof.context -> string -> xstring + val extern_fixed: Proof.context -> string -> string + val extern_entity: Proof.context -> string -> string val markup_const: Proof.context -> string -> string val pretty_const: Proof.context -> string -> Pretty.T val transfer: theory -> Proof.context -> Proof.context @@ -248,7 +253,8 @@ {mode: mode, (*inner syntax mode*) syntax: Local_Syntax.T, (*local syntax*) tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) - consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) + consts: Symset.T * Consts.T * Consts.T, + (*exclude consts, local/global consts -- local name space / abbrevs only*) facts: Facts.T, (*local facts, based on initial global facts*) cases: cases}; (*named case contexts*) @@ -262,7 +268,7 @@ make_data (mode_default, Local_Syntax.init thy, (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), - (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), + (Symset.empty, Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), Global_Theory.facts_of thy, empty_cases); ); @@ -299,6 +305,8 @@ map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, f consts, facts, cases)); +fun map_local_consts f = map_consts (fn (a, b, c) => (a, f b, c)); + fun map_facts_result f = map_data_result (fn (mode, syntax, tsig, consts, facts, cases) => let val (res, facts') = f facts @@ -323,7 +331,8 @@ fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt); -val consts_of = #1 o #consts o rep_data; +val exclude_consts_of = #1 o #consts o rep_data; +val consts_of = #2 o #consts o rep_data; val cases_of = #cases o rep_data; @@ -351,11 +360,37 @@ val concealed = map_naming Name_Space.concealed; +(* const vs. free *) + +val const_space = Consts.space_of o consts_of; + +fun is_const_declared ctxt x = + let val space = const_space ctxt + in Name_Space.declared space (Name_Space.intern space x) end; + +fun lookup_free ctxt x = + if Variable.is_const ctxt x then NONE + else + (case Variable.lookup_fixed ctxt x of + NONE => + let + val is_const = Long_Name.is_qualified x orelse is_const_declared ctxt x; + val is_free_declared = is_some (Variable.default_type ctxt x); + in if not is_const orelse is_free_declared then SOME x else NONE end + | fixed => fixed); + +fun printable_const ctxt x = + is_none (lookup_free ctxt x) andalso + not (Symset.member (exclude_consts_of ctxt) x); + +fun exclude_consts names2 = + map_consts (fn (names1, consts, thy_consts) => (Symset.union names1 names2, consts, thy_consts)); + + (* name spaces *) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; -val const_space = Consts.space_of o consts_of; fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt)); @@ -365,7 +400,16 @@ fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt); fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt); -fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt); +fun extern_const ctxt = Name_Space.extern_if (printable_const ctxt) ctxt (const_space ctxt); +fun extern_fixed ctxt x = if Name.is_skolem x then Variable.revert_fixed ctxt x else x; + +fun extern_entity ctxt = + Lexicon.unmark + {case_class = extern_class ctxt, + case_type = extern_type ctxt, + case_const = extern_const ctxt, + case_fixed = extern_fixed ctxt, + case_default = I}; fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup; fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup; @@ -391,10 +435,10 @@ if Type.eq_tsig (thy_tsig, global_tsig) then tsig else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) end) |> - map_consts (fn consts as (local_consts, global_consts) => + map_consts (fn consts as (exclude_consts, local_consts, global_consts) => let val thy_consts = Sign.consts_of thy in if Consts.eq_consts (thy_consts, global_consts) then consts - else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) + else (exclude_consts, Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) end) end; @@ -434,7 +478,7 @@ in (markups, xname) end; fun pretty_thm_name ctxt (name, i) = - Facts.pretty_thm_name (Context.Proof ctxt) (facts_of_fact ctxt name) (name, i); + Facts.pretty_thm_name ctxt (facts_of_fact ctxt name) (name, i); val print_thm_name = Pretty.string_of oo pretty_thm_name; @@ -571,24 +615,28 @@ Name.reject_internal (c, ps) handle ERROR msg => error (msg ^ consts_completion_message ctxt (c, ps)); fun err msg = error (msg ^ Position.here_list ps); + + val fixed = if proper then NONE else Variable.lookup_fixed ctxt c; + val const = Variable.lookup_const ctxt c; val consts = consts_of ctxt; - val fixed = if proper then NONE else Variable.lookup_fixed ctxt c; + val (t, reports) = - (case (fixed, Variable.lookup_const ctxt c) of - (SOME x, NONE) => - let - val reports = ps - |> filter (Context_Position.is_reported ctxt) - |> map (fn pos => (pos, Markup.name x (Variable.markup ctxt x))); - in (Free (x, infer_type ctxt (x, dummyT)), reports) end - | (_, SOME d) => - let - val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg; - val reports = ps - |> filter (Context_Position.is_reported ctxt) - |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d)); - in (Const (d, T), reports) end - | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps)); + if is_some fixed andalso is_none const then + let + val x = the fixed; + val reports = ps + |> filter (Context_Position.is_reported ctxt) + |> map (fn pos => (pos, Markup.name x (Variable.markup ctxt x))); + in (Free (x, infer_type ctxt (x, dummyT)), reports) end + else if is_some const then + let + val d = the const; + val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg; + val reports = ps + |> filter (Context_Position.is_reported ctxt) + |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d)); + in (Const (d, T), reports) end + else Consts.check_const (Context.Proof ctxt) consts (c, ps); val _ = (case (strict, t) of (true, Const (d, _)) => @@ -1206,7 +1254,7 @@ (* aliases *) fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; -fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; +fun const_alias b c ctxt = map_local_consts (Consts.alias (naming_of ctxt) b c) ctxt; (* local constants *) @@ -1216,7 +1264,7 @@ fun prepT raw_T = let val T = cert_typ ctxt raw_T in cert_term ctxt (Const (c, T)); T end; - in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; + in ctxt |> map_local_consts (Consts.constrain (c, Option.map prepT opt_T)) end; fun add_abbrev mode (b, raw_t) ctxt = let @@ -1227,12 +1275,12 @@ |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t); in ctxt - |> (map_consts o apfst) (K consts') + |> map_local_consts (K consts') |> Variable.declare_term rhs |> pair (lhs, rhs) end; -fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); +fun revert_abbrev mode c = map_local_consts (Consts.revert_abbrev mode c); fun generic_add_abbrev mode arg = Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); @@ -1471,9 +1519,9 @@ fun pretty_abbrevs verbose show_globals ctxt = let val space = const_space ctxt; - val (constants, global_constants) = - apply2 (#constants o Consts.dest) (#consts (rep_data ctxt)); - val globals = Symtab.make global_constants; + val (_, consts, global_consts) = #consts (rep_data ctxt); + val constants = #constants (Consts.dest consts); + val globals = Symtab.make (#constants (Consts.dest global_consts)); fun add_abbr (_, (_, NONE)) = I | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I diff -r 41b387d47739 -r 692241432a99 src/Pure/Isar/subgoal.ML --- a/src/Pure/Isar/subgoal.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Isar/subgoal.ML Fri Dec 06 21:27:07 2024 +0100 @@ -171,7 +171,7 @@ val subgoal = #1 (Logic.dest_implies (Thm.prop_of st)); val subgoal_params = map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal) - |> Term.variant_frees subgoal |> map #1; + |> Syntax_Trans.variant_bounds ctxt subgoal |> map #1; val n = length subgoal_params; val m = length raw_param_specs; diff -r 41b387d47739 -r 692241432a99 src/Pure/Isar/target_context.ML --- a/src/Pure/Isar/target_context.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Isar/target_context.ML Fri Dec 06 21:27:07 2024 +0100 @@ -25,7 +25,7 @@ fun context_begin_named_cmd raw_includes ("-", _) thy = Named_Target.init (prep_includes thy raw_includes) "" thy | context_begin_named_cmd raw_includes name thy = - Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy; + Named_Target.init (prep_includes thy raw_includes) (Locale.check_global thy name) thy; val end_named_cmd = Context.Theory o Local_Theory.exit_global; diff -r 41b387d47739 -r 692241432a99 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Proof/extraction.ML Fri Dec 06 21:27:07 2024 +0100 @@ -505,6 +505,8 @@ fun extract thm_vss thy = let val thy' = add_syntax thy; + val global_ctxt = Syntax.init_pretty_global thy'; + val print_thm_name = Global_Theory.print_thm_name global_ctxt; val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} = ExtractionData.get thy; @@ -640,8 +642,7 @@ let val _ = T = nullT orelse error "corr: internal error"; val _ = - msg d ("Building correctness proof for " ^ - quote (Global_Theory.print_thm_name thy thm_name) ^ + msg d ("Building correctness proof for " ^ quote (print_thm_name thm_name) ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); val prf' = prep (Proofterm.reconstruct_proof thy' prop prf); @@ -670,8 +671,8 @@ | SOME rs => (case find vs' rs of SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs') | NONE => error ("corr: no realizer for instance of theorem " ^ - quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^ - Syntax.string_of_term_global thy' + quote (print_thm_name thm_name) ^ ":\n" ^ + Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))) end @@ -686,7 +687,7 @@ SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye), defs) | NONE => error ("corr: no realizer for instance of axiom " ^ - quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm + quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))) end @@ -738,7 +739,7 @@ NONE => let val _ = - msg d ("Extracting " ^ quote (Global_Theory.print_thm_name thy' thm_name) ^ + msg d ("Extracting " ^ quote (print_thm_name thm_name) ^ (if null vs' then "" else " (relevant variables: " ^ commas_quote vs' ^ ")")); val prf' = prep (Proofterm.reconstruct_proof thy' prop prf); @@ -790,8 +791,8 @@ | SOME rs => (case find vs' rs of SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of theorem " ^ - quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^ - Syntax.string_of_term_global thy' (Envir.beta_norm + quote (print_thm_name thm_name) ^ ":\n" ^ + Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))) end @@ -803,7 +804,7 @@ case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of SOME (t, _) => (subst_TVars tye' t, defs) | NONE => error ("extr: no realizer for instance of axiom " ^ - quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm + quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))) end @@ -817,7 +818,7 @@ val name = Thm.derivation_name thm; val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else (); val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ - quote (Global_Theory.print_thm_name thy' name) ^ " has no computational content") + quote (print_thm_name name) ^ " has no computational content") in Proofterm.reconstruct_proof thy' prop prf end; val defs = diff -r 41b387d47739 -r 692241432a99 src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Proof/proof_checker.ML Fri Dec 06 21:27:07 2024 +0100 @@ -72,7 +72,10 @@ end; fun thm_of_proof thy = - let val lookup = lookup_thm thy in + let + val global_ctxt = Syntax.init_pretty_global thy; + val lookup = lookup_thm thy; + in fn prf => let val prf_names = @@ -96,9 +99,9 @@ if is_equal prop prop' then () else error ("Duplicate use of theorem name " ^ - quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos - ^ "\n" ^ Syntax.string_of_term_global thy prop - ^ "\n\n" ^ Syntax.string_of_term_global thy prop'); + quote (Global_Theory.print_thm_name global_ctxt thm_name) ^ Position.here thm_pos + ^ "\n" ^ Syntax.string_of_term global_ctxt prop + ^ "\n\n" ^ Syntax.string_of_term global_ctxt prop'); in thm_of_atom thm Ts end | thm_of _ _ (PAxm (name, _, SOME Ts)) = diff -r 41b387d47739 -r 692241432a99 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Pure.thy Fri Dec 06 21:27:07 2024 +0100 @@ -1210,7 +1210,8 @@ Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; - val name = Locale.check thy raw_name; + val ctxt = Toplevel.context_of state; + val name = Locale.check ctxt raw_name; in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = @@ -1219,9 +1220,9 @@ (Parse.name_position >> (fn raw_name => Toplevel.keep (fn state => let + val thy = Toplevel.theory_of state; val ctxt = Toplevel.context_of state; - val thy = Toplevel.theory_of state; - val name = Locale.check thy raw_name; + val name = Locale.check ctxt raw_name; in Pretty.writeln (Locale.pretty_registrations ctxt name) end))); val _ = @@ -1257,12 +1258,16 @@ val _ = Outer_Syntax.command \<^command_keyword>\locale_deps\ "visualize locale dependencies" - (Scan.succeed - (Toplevel.keep (Toplevel.theory_of #> (fn thy => + (Scan.succeed (Toplevel.keep (fn state => + let + val thy = Toplevel.theory_of state; + val ctxt = Toplevel.context_of state; + in Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => - ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) - |> Graph_Display.display_graph_old)))); + ((name, Graph_Display.content_node (Locale.extern ctxt name) [body]), parents)) + |> Graph_Display.display_graph_old + end))); val _ = Outer_Syntax.command \<^command_keyword>\print_term_bindings\ @@ -1373,10 +1378,8 @@ "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => - let - val thy = Toplevel.theory_of st; - val ctxt = Toplevel.context_of st; - in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); + let val ctxt = Toplevel.context_of st + in Pretty.writeln (Thm_Deps.pretty_thm_deps ctxt (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ diff -r 41b387d47739 -r 692241432a99 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Dec 06 21:27:07 2024 +0100 @@ -65,15 +65,14 @@ Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; fun markup_entity_cache ctxt = - Symtab.unsynchronized_cache (fn c => + Symtab.apply_unsynchronized_cache (fn c => Syntax.get_consts (Proof_Context.syntax_of ctxt) c |> maps (Lexicon.unmark {case_class = markup_class ctxt, case_type = markup_type ctxt, case_const = markup_const ctxt, case_fixed = markup_free ctxt, - case_default = K []})) - |> #apply; + case_default = K []})); @@ -265,26 +264,10 @@ Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps) |>> dest_Const_name; -local - -fun get_free ctxt x = - let - val fixed = Variable.lookup_fixed ctxt x; - val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x; - val is_declared = is_some (Variable.def_type ctxt false (x, ~1)); - in - if Variable.is_const ctxt x then NONE - else if is_some fixed then fixed - else if not is_const orelse is_declared then SOME x - else NONE - end; - -in - fun decode_term ctxt = let - val markup_free_cache = #apply (Symtab.unsynchronized_cache (markup_free ctxt)); - val markup_const_cache = #apply (Symtab.unsynchronized_cache (markup_const ctxt)); + val markup_free_cache = Symtab.apply_unsynchronized_cache (markup_free ctxt); + val markup_const_cache = Symtab.apply_unsynchronized_cache (markup_const ctxt); fun decode (result as (_: Position.report_text list, Exn.Exn _)) = result | decode (reports0, Exn.Res tm) = @@ -319,7 +302,7 @@ | decode ps _ _ (Free (a, T)) = ((Name.reject_internal (a, ps) handle ERROR msg => error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps))); - (case get_free ctxt a of + (case Proof_Context.lookup_free ctxt a of SOME x => (report ps markup_free_cache x; Free (x, T)) | NONE => let @@ -337,8 +320,6 @@ in decode end; -end; - (** parse **) @@ -731,11 +712,8 @@ local -fun extern_fixed ctxt x = - if Name.is_skolem x then Variable.revert_fixed ctxt x else x; - fun extern_cache ctxt = - Symtab.unsynchronized_cache (fn c => + Symtab.apply_unsynchronized_cache (fn c => (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of [b] => b | bs => @@ -743,41 +721,52 @@ [] => c | [b] => b | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs))) - |> Lexicon.unmark - {case_class = Proof_Context.extern_class ctxt, - case_type = Proof_Context.extern_type ctxt, - case_const = Proof_Context.extern_const ctxt, - case_fixed = extern_fixed ctxt, - case_default = I}) - |> #apply; + |> Proof_Context.extern_entity ctxt); val var_or_skolem_cache = - Symtab.unsynchronized_cache (fn s => + Symtab.apply_unsynchronized_cache (fn s => (case Lexicon.read_variable s of SOME (x, i) => (case try Name.dest_skolem x of SOME x' => (Markup.skolem, Term.string_of_vname (x', i)) | NONE => (Markup.var, s)) - | NONE => (Markup.var, s))) - |> #apply; + | NONE => (Markup.var, s))); val typing_elem = YXML.output_markup_elem Markup.typing; val sorting_elem = YXML.output_markup_elem Markup.sorting; -fun unparse_t t_to_ast pretty_flags language_markup ctxt t = +fun exclude_consts ast ctxt = let + val s = the_default "" (Syntax_Trans.default_struct ctxt); + + fun exclude (Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]) = Symset.insert s + | exclude (Ast.Constant c) = + if Lexicon.is_fixed c then Symset.insert (Lexicon.unmark_fixed c) else I + | exclude (Ast.Appl [Ast.Constant "_bound", Ast.Variable x]) = Symset.insert x + | exclude (Ast.Appl [Ast.Constant "_free", Ast.Variable x]) = Symset.insert x + | exclude (Ast.Appl asts) = fold exclude asts + | exclude _ = I; + in Proof_Context.exclude_consts (Symset.build (exclude ast)) ctxt end; + +fun unparse_t t_to_ast pretty_flags language_markup ctxt0 t = + let + val syn = Proof_Context.syntax_of ctxt0; + val prtabs = Syntax.print_mode_tabs syn; + val trf = Syntax.print_ast_translation syn; + + val ast = t_to_ast ctxt0 (Syntax.print_translation syn) t; + val ctxt = exclude_consts ast ctxt0; + val show_markup = Config.get ctxt show_markup; val show_sorts = Config.get ctxt show_sorts; val show_types = Config.get ctxt show_types orelse show_sorts; - val syn = Proof_Context.syntax_of ctxt; - val prtabs = Syntax.print_mode_tabs syn; - val trf = Syntax.print_ast_translation syn; val markup = markup_entity_cache ctxt; val extern = extern_cache ctxt; val free_or_skolem_cache = - #apply (Symtab.unsynchronized_cache (fn x => (markup_free ctxt x, extern_fixed ctxt x))); + Symtab.apply_unsynchronized_cache (fn x => + (markup_free ctxt x, Proof_Context.extern_fixed ctxt x)); val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); @@ -829,8 +818,7 @@ in Unsynchronized.change cache (Ast.Table.update (A, block)); block end) end; in - t_to_ast ctxt (Syntax.print_translation syn) t - |> Ast.normalize ctxt {permissive_constraints = true} (Syntax.print_rules syn) + Ast.normalize ctxt {permissive_constraints = true} (Syntax.print_rules syn) ast |> pretty_ast pretty_flags language_markup end; diff -r 41b387d47739 -r 692241432a99 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Syntax/syntax_trans.ML Fri Dec 06 21:27:07 2024 +0100 @@ -31,13 +31,14 @@ val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val mark_bound_abs: string * typ -> term val mark_bound_body: string * typ -> term - val bound_vars: (string * typ) list -> term -> term + val variant_bounds: Proof.context -> term -> (string * 'a) list -> (string * 'a) list + val bound_vars: Proof.context -> (string * typ) list -> term -> term val abs_tr': Proof.context -> term -> term - val atomic_abs_tr': string * typ * term -> term * term + val atomic_abs_tr': Proof.context -> string * typ * term -> term * term val const_abs_tr': term -> term val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term) - val preserve_binder_abs_tr': string -> typ -> term list -> term - val preserve_binder_abs2_tr': string -> typ -> term list -> term + val preserve_binder_abs_tr': string -> Proof.context -> typ -> term list -> term + val preserve_binder_abs2_tr': string -> Proof.context -> typ -> term list -> term val print_abs: string * typ * term -> string * term val dependent_tr': string * string -> term list -> term val antiquote_tr': string -> term -> term @@ -47,6 +48,7 @@ val update_name_tr': term -> term val get_idents: Proof.context -> {structs: string list, fixes: string list} val put_idents: {structs: string list, fixes: string list} -> Proof.context -> Proof.context + val default_struct: Proof.context -> string option val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list val pure_parse_translation: (string * (Proof.context -> term list -> term)) list val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list @@ -75,7 +77,6 @@ (print_mode_value ()) <> SOME type_bracketsN; - (** parse (ast) translations **) (* strip_positions *) @@ -224,6 +225,8 @@ val get_idents = Idents.get; val put_idents = Idents.put; +val default_struct = try hd o #structs o get_idents; + fun indexdefault_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]] @@ -239,9 +242,9 @@ | index_tr ts = raise TERM ("index_tr", ts); fun struct_tr ctxt [Const ("_indexdefault", _)] = - (case #structs (get_idents ctxt) of - x :: _ => Syntax.const (Lexicon.mark_fixed x) - | _ => error "Illegal reference to implicit structure") + (case default_struct ctxt of + SOME x => Syntax.const (Lexicon.mark_fixed x) + | NONE => error "Illegal reference to implicit structure") | struct_tr _ ts = raise TERM ("struct_tr", ts); @@ -301,14 +304,27 @@ fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T); fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T); -fun bound_vars vars body = - subst_bounds (map mark_bound_abs (rev (Term.variant_frees body vars)), body); +fun variant_bounds ctxt t = + let + val s = the_default "" (default_struct ctxt); -fun strip_abss vars_of body_of tm = + fun declare (Const ("_struct", _) $ Const ("_indexdefault", _)) = Name.declare s + | declare (Const (c, _)) = + if Lexicon.is_fixed c then Name.declare (Lexicon.unmark_fixed c) else I + | declare (Free (x, _)) = Name.declare x + | declare (t $ u) = declare t #> declare u + | declare (Abs (_, _, t)) = declare t + | declare _ = I; + in Name.variant_names_build (declare t) end; + +fun bound_vars ctxt vars body = + subst_bounds (map mark_bound_abs (rev (variant_bounds ctxt body vars)), body); + +fun strip_abss ctxt vars_of body_of tm = let val vars = vars_of tm; val body = body_of tm; - val new_vars = Term.variant_frees body vars; + val new_vars = variant_bounds ctxt body vars; fun subst (x, T) b = if Name.is_internal x andalso not (Term.is_dependent b) then (Const ("_idtdummy", T), incr_boundvars ~1 b) @@ -319,10 +335,10 @@ fun abs_tr' ctxt tm = uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t)) - (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); + (strip_abss ctxt strip_abs_vars strip_abs_body (eta_contr ctxt tm)); -fun atomic_abs_tr' (x, T, t) = - let val xT = singleton (Term.variant_frees t) (x, T) +fun atomic_abs_tr' ctxt (x, T, t) = + let val xT = singleton (variant_bounds ctxt t) (x, T) in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end; fun abs_ast_tr' asts = @@ -346,21 +362,21 @@ | mk_idts [idt] = idt | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts; - fun tr' t = + fun tr' ctxt t = let - val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; + val (xs, bd) = strip_abss ctxt (strip_qnt_vars name) (strip_qnt_body name) t; in Syntax.const syn $ mk_idts xs $ bd end; - fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts) - | binder_tr' [] = raise Match; - in (name, fn _ => binder_tr') end; + fun binder_tr' ctxt (t :: ts) = Term.list_comb (tr' ctxt (Syntax.const name $ t), ts) + | binder_tr' _ [] = raise Match; + in (name, binder_tr') end; -fun preserve_binder_abs_tr' syn ty (Abs abs :: ts) = - let val (x, t) = atomic_abs_tr' abs +fun preserve_binder_abs_tr' syn ctxt ty (Abs abs :: ts) = + let val (x, t) = atomic_abs_tr' ctxt abs in list_comb (Const (syn, ty) $ x $ t, ts) end; -fun preserve_binder_abs2_tr' syn ty (A :: Abs abs :: ts) = - let val (x, t) = atomic_abs_tr' abs +fun preserve_binder_abs2_tr' syn ctxt ty (A :: Abs abs :: ts) = + let val (x, t) = atomic_abs_tr' ctxt abs in list_comb (Const (syn, ty) $ x $ A $ t, ts) end; @@ -389,7 +405,7 @@ (* dependent / nondependent quantifiers *) fun print_abs (x, T, b) = - let val x' = #1 (Name.variant x (Name.build_context (Term.declare_term_names b))) + let val x' = #1 (Name.variant x (Name.build_context (Term.declare_free_names b))) in (x', subst_bound (mark_bound_abs (x', T), b)) end; fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = @@ -449,9 +465,9 @@ | index_ast_tr' _ = raise Match; fun struct_ast_tr' ctxt [Ast.Constant "_indexdefault"] = - (case #structs (get_idents ctxt) of - x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x] - | _ => raise Match) + (case default_struct ctxt of + SOME x => Ast.Appl [Ast.Constant "_free", Ast.Variable x] + | NONE => raise Match) | struct_ast_tr' _ _ = raise Match; diff -r 41b387d47739 -r 692241432a99 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Fri Dec 06 21:27:07 2024 +0100 @@ -47,8 +47,7 @@ in Proof_Context.pretty_term_abbrev ctxt' eq end; fun pretty_locale ctxt (name, pos) = - let val thy = Proof_Context.theory_of ctxt - in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end; + Pretty.str (Locale.extern ctxt (Locale.check ctxt (name, pos))); fun pretty_bundle ctxt (name, pos) = Pretty.str (Bundle.extern ctxt (Bundle.check ctxt (name, pos))); diff -r 41b387d47739 -r 692241432a99 src/Pure/consts.ML --- a/src/Pure/consts.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/consts.ML Fri Dec 06 21:27:07 2024 +0100 @@ -313,7 +313,7 @@ fun rev_abbrev lhs rhs = let val (xs, body) = strip_abss (Envir.beta_eta_contract rhs); - val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_frees body xs); + val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_bounds body xs); in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end; in diff -r 41b387d47739 -r 692241432a99 src/Pure/facts.ML --- a/src/Pure/facts.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/facts.ML Fri Dec 06 21:27:07 2024 +0100 @@ -30,7 +30,7 @@ val intern: T -> xstring -> string val extern: Proof.context -> T -> string -> xstring val markup_extern: Proof.context -> T -> string -> Markup.T * xstring - val pretty_thm_name: Context.generic -> T -> Thm_Name.T -> Pretty.T + val pretty_thm_name: Proof.context -> T -> Thm_Name.T -> Pretty.T val defined: T -> string -> bool val is_dynamic: T -> string -> bool val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option @@ -174,9 +174,9 @@ fun extern ctxt = Name_Space.extern ctxt o space_of; fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of; -fun pretty_thm_name context facts thm_name = +fun pretty_thm_name ctxt facts thm_name = let - val prfx = Thm_Name.print_prefix context (space_of facts) thm_name; + val prfx = Thm_Name.print_prefix ctxt (space_of facts) thm_name; val sffx = Thm_Name.print_suffix thm_name; in Pretty.block [Pretty.mark_str prfx, Pretty.str sffx] end; diff -r 41b387d47739 -r 692241432a99 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/global_theory.ML Fri Dec 06 21:27:07 2024 +0100 @@ -14,8 +14,8 @@ val alias_fact: binding -> string -> theory -> theory val hide_fact: bool -> string -> theory -> theory val dest_thms: bool -> theory list -> theory -> (Thm_Name.P * thm) list - val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T - val print_thm_name: theory -> Thm_Name.T -> string + val pretty_thm_name: Proof.context -> Thm_Name.T -> Pretty.T + val print_thm_name: Proof.context -> Thm_Name.T -> string val get_thm_names: theory -> Thm_Name.P Inttab.table val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option @@ -88,7 +88,9 @@ Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy) |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms); -fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy); +fun pretty_thm_name ctxt = + Facts.pretty_thm_name ctxt (facts_of (Proof_Context.theory_of ctxt)); + val print_thm_name = Pretty.string_of oo pretty_thm_name; @@ -108,9 +110,11 @@ else (case Inttab.lookup thm_names serial of SOME (thm_name', thm_pos') => - raise THM ("Duplicate use of derivation identity for " ^ - print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^ - print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm]) + let val thy_ctxt = Proof_Context.init_global thy in + raise THM ("Duplicate use of derivation identity for " ^ + print_thm_name thy_ctxt thm_name ^ Position.here thm_pos ^ " vs. " ^ + print_thm_name thy_ctxt thm_name' ^ Position.here thm_pos', 0, [thm]) + end | NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names))); fun lazy_thm_names thy = diff -r 41b387d47739 -r 692241432a99 src/Pure/logic.ML --- a/src/Pure/logic.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/logic.ML Fri Dec 06 21:27:07 2024 +0100 @@ -667,7 +667,7 @@ (*reverses parameters for substitution*) fun goal_params st i = let val gi = get_goal st i - val rfrees = map Free (rev (Term.variant_frees gi (strip_params gi))) + val rfrees = map Free (rev (Term.variant_bounds gi (strip_params gi))) in (gi, rfrees) end; fun concl_of_goal st i = diff -r 41b387d47739 -r 692241432a99 src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/primitive_defs.ML Fri Dec 06 21:27:07 2024 +0100 @@ -31,7 +31,7 @@ val eq_body = Term.strip_all_body eq; val display_terms = - commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars); + commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars ctxt eq_vars); val display_types = commas_quote o map (Syntax.string_of_typ ctxt); val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\)"; @@ -77,7 +77,7 @@ fun abs_def eq = let val body = Term.strip_all_body eq; - val vars = map Free (Term.variant_frees body (Term.strip_all_vars eq)); + val vars = map Free (Term.variant_bounds body (Term.strip_all_vars eq)); val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (rev vars, body)); val (lhs', args) = Term.strip_comb lhs; val rhs' = fold_rev (absfree o dest_Free) args rhs; diff -r 41b387d47739 -r 692241432a99 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/raw_simplifier.ML Fri Dec 06 21:27:07 2024 +0100 @@ -481,10 +481,9 @@ fun print_thm ctxt msg (name, th) = let - val thy = Proof_Context.theory_of ctxt; val sffx = if Thm_Name.is_empty name then "" - else " " ^ quote (Global_Theory.print_thm_name thy name) ^ ":"; + else " " ^ quote (Global_Theory.print_thm_name ctxt name) ^ ":"; in print_term ctxt (msg ^ sffx) (Thm.full_prop_of th) end; fun print_thm0 ctxt msg th = print_thm ctxt msg (Thm_Name.empty, th); diff -r 41b387d47739 -r 692241432a99 src/Pure/term.ML --- a/src/Pure/term.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/term.ML Fri Dec 06 21:27:07 2024 +0100 @@ -157,6 +157,7 @@ val declare_tvar_names: (int -> bool) -> term -> Name.context -> Name.context val declare_free_names: term -> Name.context -> Name.context val declare_var_names: (int -> bool) -> term -> Name.context -> Name.context + val variant_bounds: term -> (string * 'a) list -> (string * 'a) list val hidden_polymorphism: term -> (indexname * sort) list val declare_term_names: term -> Name.context -> Name.context val variant_frees: term -> (string * 'a) list -> (string * 'a) list @@ -583,6 +584,8 @@ val declare_free_names = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); fun declare_var_names pred = fold_aterms (fn Var ((x, i), _) => pred i ? Name.declare x | _ => I); +fun variant_bounds t = Name.variant_names_build (declare_free_names t); + (*extra type variables in a term, not covered by its type*) fun hidden_polymorphism t = let diff -r 41b387d47739 -r 692241432a99 src/Pure/term_items.ML --- a/src/Pure/term_items.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/term_items.ML Fri Dec 06 21:27:07 2024 +0100 @@ -36,6 +36,7 @@ val make3: key * 'a -> key * 'a -> key * 'a -> 'a table type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}; val unsynchronized_cache: (key -> 'a) -> 'a cache_ops + val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a type set = int table val add_set: key -> set -> set val make_set: key list -> set @@ -89,6 +90,7 @@ type 'a cache_ops = 'a Table.cache_ops; val unsynchronized_cache = Table.unsynchronized_cache; +val apply_unsynchronized_cache = Table.apply_unsynchronized_cache; (* set with order of addition *) diff -r 41b387d47739 -r 692241432a99 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/thm.ML Fri Dec 06 21:27:07 2024 +0100 @@ -1095,8 +1095,8 @@ SOME T' => T' | NONE => raise Fail "strip_shyps: bad type variable in proof term")); val map_ztyp = - #apply (ZTypes.unsynchronized_cache - (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar))); + ZTypes.apply_unsynchronized_cache + (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar)); val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof; val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof; diff -r 41b387d47739 -r 692241432a99 src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/thm_deps.ML Fri Dec 06 21:27:07 2024 +0100 @@ -11,7 +11,7 @@ val has_skip_proof: thm list -> bool val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list - val pretty_thm_deps: theory -> thm list -> Pretty.T + val pretty_thm_deps: Proof.context -> thm list -> Pretty.T val unused_thms_cmd: theory list * theory list -> (Thm_Name.T * thm) list end; @@ -71,10 +71,11 @@ |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I) end; -fun pretty_thm_deps thy thms = +fun pretty_thm_deps ctxt thms = let + val thy = Proof_Context.theory_of ctxt; val facts = Global_Theory.facts_of thy; - val extern_fact = Name_Space.extern_generic (Context.Theory thy) (Facts.space_of facts); + val extern_fact = Name_Space.extern ctxt (Facts.space_of facts); val deps = (case try (thm_deps thy) thms of SOME deps => deps @@ -83,7 +84,7 @@ deps |> map (fn (_, thm_name as (name, _)) => (extern_fact name, thm_name)) |> sort_by #1 - |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name thy thm_name]) + |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name ctxt thm_name]) in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; diff -r 41b387d47739 -r 692241432a99 src/Pure/thm_name.ML --- a/src/Pure/thm_name.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/thm_name.ML Fri Dec 06 21:27:07 2024 +0100 @@ -23,7 +23,7 @@ val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list val parse: string -> T - val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string + val print_prefix: Proof.context -> Name_Space.T -> T -> Markup.T * string val print_suffix: T -> string val print: T -> string val print_pos: P -> string @@ -99,9 +99,9 @@ (* print *) -fun print_prefix context space ((name, _): T) = +fun print_prefix ctxt space ((name, _): T) = if name = "" then (Markup.empty, "") - else (Name_Space.markup space name, Name_Space.extern_generic context space name); + else (Name_Space.markup space name, Name_Space.extern ctxt space name); fun print_suffix (name, index) = if name = "" orelse index = 0 then "" diff -r 41b387d47739 -r 692241432a99 src/Pure/type_infer_context.ML --- a/src/Pure/type_infer_context.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/type_infer_context.ML Fri Dec 06 21:27:07 2024 +0100 @@ -248,7 +248,7 @@ val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts); val (Ts', Ts'') = chop (length Ts) Ts_bTs'; fun prep t = - let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) + let val xs = rev (Syntax_Trans.variant_bounds ctxt t (rev (map fst bs ~~ Ts''))) in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end; in (map prep ts', Ts') end; diff -r 41b387d47739 -r 692241432a99 src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/variable.ML Fri Dec 06 21:27:07 2024 +0100 @@ -326,7 +326,7 @@ [] => t | bounds => let - val names = Term.declare_term_names t (names_of ctxt); + val names = Term.declare_free_names t (names_of ctxt); val xs = rev (Name.variants names (rev (map #2 bounds))); fun substs (((b, T), _), x') = let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U)) @@ -705,7 +705,7 @@ fun focus_params bindings t ctxt = let - val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :-*) + val ps = Syntax_Trans.variant_bounds ctxt t (Term.strip_all_vars t); val (xs, Ts) = split_list ps; val (xs', ctxt') = (case bindings of diff -r 41b387d47739 -r 692241432a99 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Pure/zterm.ML Fri Dec 06 21:27:07 2024 +0100 @@ -548,7 +548,7 @@ fun instantiate_type_same instT = if ZTVars.is_empty instT then Same.same - else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)))); + else ZTypes.apply_unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))); fun instantiate_term_same typ inst = subst_term_same typ (Same.function (ZVars.lookup inst)); @@ -863,9 +863,7 @@ let val lookup = if Vartab.is_empty tenv then K NONE - else - #apply (ZVars.unsynchronized_cache - (apsnd typ_of #> Envir.lookup envir #> Option.map zterm)); + else ZVars.apply_unsynchronized_cache (apsnd typ_of #> Envir.lookup envir #> Option.map zterm); val normT = norm_type_same ztyp tyenv; @@ -1008,8 +1006,8 @@ val typ_operation = #typ_operation ucontext {strip_sorts = true}; val unconstrain_typ = Same.commit typ_operation; val unconstrain_ztyp = - #apply (ZTypes.unsynchronized_cache - (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of))); + ZTypes.apply_unsynchronized_cache + (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)); val unconstrain_zterm = zterm o Term.map_types typ_operation; val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp); @@ -1226,10 +1224,10 @@ val typ = if Names.is_empty tfrees then Same.same else - #apply (ZTypes.unsynchronized_cache + ZTypes.apply_unsynchronized_cache (subst_type_same (fn ((a, i), S) => if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S) - else raise Same.SAME))); + else raise Same.SAME)); val term = subst_term_same typ (fn ((x, i), T) => if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T) @@ -1251,10 +1249,10 @@ let val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b))); val typ = - #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v => + ZTypes.apply_unsynchronized_cache (subst_type_same (fn v => (case ZTVars.lookup tab v of NONE => raise Same.SAME - | SOME w => ZTVar w)))); + | SOME w => ZTVar w))); in map_proof_types {hyps = false} typ prf end; fun legacy_freezeT_proof t prf = @@ -1263,7 +1261,7 @@ | SOME f => let val tvar = ztyp_of o Same.function f; - val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)); + val typ = ZTypes.apply_unsynchronized_cache (subst_type_same tvar); in map_proof_types {hyps = false} typ prf end); @@ -1297,7 +1295,7 @@ if inc = 0 then Same.same else let fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME - in #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end; + in ZTypes.apply_unsynchronized_cache (subst_type_same tvar) end; fun incr_indexes_proof inc prf = let @@ -1437,8 +1435,8 @@ val typ_cache = typ_cache thy; val typ = - #apply (ZTypes.unsynchronized_cache - (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of)); + ZTypes.apply_unsynchronized_cache + (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of); val typ_sort = #typ_operation ucontext {strip_sorts = false}; diff -r 41b387d47739 -r 692241432a99 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Tools/induct.ML Fri Dec 06 21:27:07 2024 +0100 @@ -607,7 +607,7 @@ let val maxidx = Thm.maxidx_of st; val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) - val params = Term.variant_frees goal (Logic.strip_params goal); + val params = Syntax_Trans.variant_bounds ctxt goal (Logic.strip_params goal); in if not (null params) then (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ diff -r 41b387d47739 -r 692241432a99 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Thu Dec 05 19:44:53 2024 +0100 +++ b/src/Tools/subtyping.ML Fri Dec 06 21:27:07 2024 +0100 @@ -244,7 +244,7 @@ val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts); val (Ts', Ts'') = chop (length Ts) Ts_bTs'; fun prep t = - let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts''))) + let val xs = rev (Syntax_Trans.variant_bounds ctxt t (rev (map fst bs ~~ Ts''))) in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end; in (map prep ts', Ts') end;