# HG changeset patch # User wenzelm # Date 1733488405 -3600 # Node ID fa37ee54644c4b3b9dd6fcb93d7ee07c0c7f409b # Parent e2ab4147b244b50d1a4ba2f4dd89ce1378dadf25 clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed"); diff -r e2ab4147b244 -r fa37ee54644c src/HOL/Auth/Guard/Proto.thy --- a/src/HOL/Auth/Guard/Proto.thy Tue Dec 03 22:46:24 2024 +0100 +++ b/src/HOL/Auth/Guard/Proto.thy Fri Dec 06 13:33:25 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 e2ab4147b244 -r fa37ee54644c src/HOL/Hoare_Parallel/RG_Examples.thy --- a/src/HOL/Hoare_Parallel/RG_Examples.thy Tue Dec 03 22:46:24 2024 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Fri Dec 06 13:33:25 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 e2ab4147b244 -r fa37ee54644c src/HOL/Nominal/Examples/Class2.thy --- a/src/HOL/Nominal/Examples/Class2.thy Tue Dec 03 22:46:24 2024 +0100 +++ b/src/HOL/Nominal/Examples/Class2.thy Fri Dec 06 13:33:25 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 e2ab4147b244 -r fa37ee54644c src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Dec 06 13:33:25 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 e2ab4147b244 -r fa37ee54644c src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Dec 06 13:33:25 2024 +0100 @@ -43,6 +43,8 @@ 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 @@ -251,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*) @@ -265,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); ); @@ -302,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 @@ -326,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; @@ -373,6 +379,13 @@ 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 *) @@ -387,7 +400,7 @@ 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_if (is_none o lookup_free ctxt) 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 = @@ -422,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; @@ -1241,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 *) @@ -1251,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 @@ -1262,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); @@ -1506,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 e2ab4147b244 -r fa37ee54644c src/Pure/Isar/subgoal.ML --- a/src/Pure/Isar/subgoal.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Pure/Isar/subgoal.ML Fri Dec 06 13:33:25 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; + |> Term.variant_bounds subgoal |> map #1; val n = length subgoal_params; val m = length raw_param_specs; diff -r e2ab4147b244 -r fa37ee54644c src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Dec 06 13:33:25 2024 +0100 @@ -735,15 +735,27 @@ 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 = +val exclude_consts = let + fun 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 o Symset.build o exclude 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; @@ -801,8 +813,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 e2ab4147b244 -r fa37ee54644c src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Pure/Syntax/syntax_trans.ML Fri Dec 06 13:33:25 2024 +0100 @@ -302,13 +302,13 @@ 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); + subst_bounds (map mark_bound_abs (rev (Term.variant_bounds body vars)), body); fun strip_abss 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 = Term.variant_bounds 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) @@ -322,7 +322,7 @@ (strip_abss 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) + let val xT = singleton (Term.variant_bounds t) (x, T) in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end; fun abs_ast_tr' asts = @@ -389,7 +389,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) = diff -r e2ab4147b244 -r fa37ee54644c src/Pure/type_infer_context.ML --- a/src/Pure/type_infer_context.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Pure/type_infer_context.ML Fri Dec 06 13:33:25 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 (Term.variant_bounds 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 e2ab4147b244 -r fa37ee54644c src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Pure/variable.ML Fri Dec 06 13:33:25 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 = Term.variant_bounds t (Term.strip_all_vars t); val (xs, Ts) = split_list ps; val (xs', ctxt') = (case bindings of diff -r e2ab4147b244 -r fa37ee54644c src/Tools/induct.ML --- a/src/Tools/induct.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Tools/induct.ML Fri Dec 06 13:33:25 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 = Term.variant_bounds goal (Logic.strip_params goal); in if not (null params) then (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^ diff -r e2ab4147b244 -r fa37ee54644c src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Tue Dec 03 22:46:24 2024 +0100 +++ b/src/Tools/subtyping.ML Fri Dec 06 13:33:25 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 (Term.variant_bounds 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;