# HG changeset patch # User wenzelm # Date 1629987888 -7200 # Node ID 10455384a3e5197fd10b228237fb361bfed03d37 # Parent bf9871795aeb426411fbf228dfa39914e6e6d0d4# Parent c36b663ef037606fea5b493728a10d32b5b3f574 merged diff -r bf9871795aeb -r 10455384a3e5 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Doc/Implementation/Logic.thy Thu Aug 26 16:24:48 2021 +0200 @@ -585,7 +585,7 @@ @{define_ML Thm.forall_elim: "cterm -> thm -> thm"} \\ @{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ @{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\ - @{define_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ + @{define_ML Thm.generalize: "Symtab.set * Symtab.set -> int -> thm -> thm"} \\ @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"} \\ @{define_ML Thm.add_axiom: "Proof.context -> @@ -646,8 +646,8 @@ \<^descr> \<^ML>\Thm.generalize\~$\<^vec>\, \<^vec>x)\ corresponds to the \generalize\ rules of \figref{fig:subst-rules}. Here collections of type and - term variables are generalized simultaneously, specified by the given basic - names. + term variables are generalized simultaneously, specified by the given sets of + basic names. \<^descr> \<^ML>\Thm.instantiate\~\(\<^vec>\\<^sub>s, \<^vec>x\<^sub>$\ corresponds to the \instantiate\ rules of \figref{fig:subst-rules}. Type variables are diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Eisbach/match_method.ML Thu Aug 26 16:24:48 2021 +0200 @@ -173,7 +173,7 @@ val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms |> Conjunction.intr_balanced - |> Drule.generalize ([], map fst abs_nms) + |> Drule.generalize (Symtab.empty, Symtab.make_set (map fst abs_nms)) |> Thm.tag_free_dummy; val atts = map (Attrib.attribute ctxt') att; diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Library/cconv.ML Thu Aug 26 16:24:48 2021 +0200 @@ -146,7 +146,8 @@ val rule = abstract_rule_thm x val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq) in - (Drule.instantiate_normalize inst rule OF [Drule.generalize ([], [u]) eq]) + (Drule.instantiate_normalize inst rule OF + [Drule.generalize (Symtab.empty, Symtab.make_set [u]) eq]) |> Drule.zero_var_indexes end diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Library/code_lazy.ML --- a/src/HOL/Library/code_lazy.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Library/code_lazy.ML Thu Aug 26 16:24:48 2021 +0200 @@ -122,7 +122,7 @@ |> Conjunction.intr_balanced |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)] |> Thm.implies_intr assum - |> Thm.generalize ([], params) 0 + |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0 |> Axclass.unoverload ctxt |> Thm.varifyT_global end @@ -494,7 +494,9 @@ val delay_dummy_thm = (pat_def_thm RS @{thm symmetric}) |> Drule.infer_instantiate' lthy10 [SOME (Thm.cterm_of lthy10 (Const (\<^const_name>\Pure.dummy_pattern\, HOLogic.unitT --> lazy_type)))] - |> Thm.generalize (map (fst o dest_TFree) type_args, []) (Variable.maxidx_of lthy10 + 1); + |> Thm.generalize + (Symtab.make_set (map (fst o dest_TFree) type_args), Symtab.empty) + (Variable.maxidx_of lthy10 + 1); val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms val ctr_thms_abs = map (fn thm => Drule.abs_def (thm RS @{thm eq_reflection})) ctrs_lazy_thms diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Aug 26 16:24:48 2021 +0200 @@ -852,7 +852,7 @@ |> unfold_thms lthy [dtor_ctor]; in (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans)) - |> Drule.generalize ([], [y_s]) + |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s]) end; val map_thms = @@ -931,7 +931,7 @@ |> infer_instantiate' lthy (replicate live NONE @ [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))]) |> unfold_thms lthy [dtor_ctor] - |> Drule.generalize ([], [y_s, z_s]) + |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s, z_s]) end; val rel_inject_thms = diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Aug 26 16:24:48 2021 +0200 @@ -160,7 +160,7 @@ val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0)); in Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split - |> Drule.generalize ([], [s]) + |> Drule.generalize (Symtab.empty, Symtab.make_set [s]) end | _ => split); diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Aug 26 16:24:48 2021 +0200 @@ -42,7 +42,7 @@ |> Conjunction.intr_balanced |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)] |> Thm.implies_intr assum - |> Thm.generalize ([], params) 0 + |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0 |> Axclass.unoverload ctxt |> Thm.varifyT_global end; diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Tools/Function/induction_schema.ML Thu Aug 26 16:24:48 2021 +0200 @@ -381,7 +381,7 @@ val res = Conjunction.intr_balanced (map_index project branches) |> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps) - |> Drule.generalize ([], [Rn]) + |> Drule.generalize (Symtab.empty, Symtab.make_set [Rn]) val nbranches = length branches val npres = length pres diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Tools/SMT/smt_replay_methods.ML --- a/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 26 16:24:48 2021 +0200 @@ -171,7 +171,7 @@ fun by_tac ctxt thms ns ts t tac = Goal.prove ctxt [] (map as_prop ts) (as_prop t) (fn {context, prems} => HEADGOAL (tac context prems)) - |> Drule.generalize ([], ns) + |> Drule.generalize (Symtab.empty, Symtab.make_set ns) |> discharge 1 thms fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac) diff -r bf9871795aeb -r 10455384a3e5 src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Thu Aug 26 16:24:48 2021 +0200 @@ -575,7 +575,7 @@ ((Name.clean_index (prep a, idx), \<^typ>\bool \ bool \ bool\), Thm.cterm_of ctxt' t) in thm - |> Thm.generalize (tfrees, rnames @ frees) idx + |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx |> Thm.instantiate (map tinst binsts, map inst binsts) end @@ -596,7 +596,7 @@ ((Name.clean_index (prep a, idx), \<^typ>\bool \ bool \ bool\), Thm.cterm_of ctxt' t) in thm - |> Thm.generalize (tfrees, rnames @ frees) idx + |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx |> Thm.instantiate (map tinst binsts, map inst binsts) end @@ -718,7 +718,8 @@ raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |> Raw_Simplifier.rewrite_rule ctxt' post_simps |> Simplifier.norm_hhf ctxt' - |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, []) + |> Drule.generalize + (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty) |> Drule.zero_var_indexes end (* @@ -753,7 +754,8 @@ raise TERM ("Transfer failed to convert goal to an object-logic formula", ts)) |> Raw_Simplifier.rewrite_rule ctxt' post_simps |> Simplifier.norm_hhf ctxt' - |> Drule.generalize (map (fst o dest_TFree o Thm.typ_of o snd) instT, []) + |> Drule.generalize + (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty) |> Drule.zero_var_indexes end diff -r bf9871795aeb -r 10455384a3e5 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/Isar/local_defs.ML Thu Aug 26 16:24:48 2021 +0200 @@ -89,7 +89,8 @@ *) fun expand defs = Drule.implies_intr_list defs - #> Drule.generalize ([], map (#1 o head_of_def o Thm.term_of) defs) + #> Drule.generalize + (Symtab.empty, fold (Symtab.insert_set o #1 o head_of_def o Thm.term_of) defs Symtab.empty) #> funpow (length defs) (fn th => Drule.reflexive_thm RS th); val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of); diff -r bf9871795aeb -r 10455384a3e5 src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/drule.ML Thu Aug 26 16:24:48 2021 +0200 @@ -52,7 +52,7 @@ sig include BASIC_DRULE val outer_params: term -> (string * typ) list - val generalize: string list * string list -> thm -> thm + val generalize: Symtab.set * Symtab.set -> thm -> thm val list_comb: cterm * cterm list -> cterm val strip_comb: cterm -> cterm * cterm list val beta_conv: cterm -> cterm -> cterm diff -r bf9871795aeb -r 10455384a3e5 src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/goal.ML Thu Aug 26 16:24:48 2021 +0200 @@ -120,6 +120,7 @@ val fixes = map (Thm.cterm_of ctxt) xs; val tfrees = fold Term.add_tfrees (prop :: As) []; + val tfrees_set = fold (Symtab.insert_set o #1) tfrees Symtab.empty; val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees; val global_prop = @@ -131,7 +132,7 @@ Drule.implies_intr_list assms #> Drule.forall_intr_list fixes #> Thm.adjust_maxidx_thm ~1 #> - Thm.generalize (map #1 tfrees, []) 0 #> + Thm.generalize (tfrees_set, Symtab.empty) 0 #> Thm.strip_shyps #> Thm.solve_constraints); val local_result = diff -r bf9871795aeb -r 10455384a3e5 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/more_thm.ML Thu Aug 26 16:24:48 2021 +0200 @@ -408,16 +408,17 @@ val idx = Thm.maxidx_of th + 1; fun index ((a, A), b) = (((a, idx), A), b); val insts = (map index instT, map index inst); - val frees = (map (#1 o #1) instT, map (#1 o #1) inst); + val tfrees = fold (Symtab.insert_set o #1 o #1) instT Symtab.empty; + val frees = fold (Symtab.insert_set o #1 o #1) inst Symtab.empty; val hyps = Thm.chyps_of th; val inst_cterm = - Thm.generalize_cterm frees idx #> + Thm.generalize_cterm (tfrees, frees) idx #> Thm.instantiate_cterm insts; in th |> fold_rev Thm.implies_intr hyps - |> Thm.generalize frees idx + |> Thm.generalize (tfrees, frees) idx |> Thm.instantiate insts |> fold (elim_implies o Thm.assume o inst_cterm) hyps end; diff -r bf9871795aeb -r 10455384a3e5 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/proofterm.ML Thu Aug 26 16:24:48 2021 +0200 @@ -113,7 +113,7 @@ val legacy_freezeT: term -> proof -> proof val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof val permute_prems_proof: term list -> int -> int -> proof -> proof - val generalize_proof: string list * string list -> int -> term -> proof -> proof + val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> proof -> proof val lift_proof: term -> int -> term -> proof -> proof @@ -949,14 +949,14 @@ fun generalize_proof (tfrees, frees) idx prop prf = let val gen = - if null frees then [] + if Symtab.is_empty frees then [] else - fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T) | _ => I) - (Term_Subst.generalize (tfrees, []) idx prop) []; + fold_aterms (fn Free (x, T) => Symtab.defined frees x ? insert (op =) (x, T) | _ => I) + (Term_Subst.generalize (tfrees, Symtab.empty) idx prop) []; in prf |> Same.commit (map_proof_terms_same - (Term_Subst.generalize_same (tfrees, []) idx) + (Term_Subst.generalize_same (tfrees, Symtab.empty) idx) (Term_Subst.generalizeT_same tfrees idx)) |> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen |> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen diff -r bf9871795aeb -r 10455384a3e5 src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/term_subst.ML Thu Aug 26 16:24:48 2021 +0200 @@ -9,10 +9,10 @@ val map_atypsT_same: typ Same.operation -> typ Same.operation val map_types_same: typ Same.operation -> term Same.operation val map_aterms_same: term Same.operation -> term Same.operation - val generalizeT_same: string list -> int -> typ Same.operation - val generalize_same: string list * string list -> int -> term Same.operation - val generalizeT: string list -> int -> typ -> typ - val generalize: string list * string list -> int -> term -> term + val generalizeT_same: Symtab.set -> int -> typ Same.operation + val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation + val generalizeT: Symtab.set -> int -> typ -> typ + val generalize: Symtab.set * Symtab.set -> int -> term -> term val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int val instantiate_maxidx: ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list -> @@ -68,32 +68,34 @@ (* generalization of fixed variables *) -fun generalizeT_same [] _ _ = raise Same.SAME - | generalizeT_same tfrees idx ty = - let - fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts) - | gen (TFree (a, S)) = - if member (op =) tfrees a then TVar ((a, idx), S) - else raise Same.SAME - | gen _ = raise Same.SAME; - in gen ty end; +fun generalizeT_same tfrees idx ty = + if Symtab.is_empty tfrees then raise Same.SAME + else + let + fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts) + | gen (TFree (a, S)) = + if Symtab.defined tfrees a then TVar ((a, idx), S) + else raise Same.SAME + | gen _ = raise Same.SAME; + in gen ty end; -fun generalize_same ([], []) _ _ = raise Same.SAME - | generalize_same (tfrees, frees) idx tm = - let - val genT = generalizeT_same tfrees idx; - fun gen (Free (x, T)) = - if member (op =) frees x then - Var (Name.clean_index (x, idx), Same.commit genT T) - else Free (x, genT T) - | gen (Var (xi, T)) = Var (xi, genT T) - | gen (Const (c, T)) = Const (c, genT T) - | gen (Bound _) = raise Same.SAME - | gen (Abs (x, T, t)) = - (Abs (x, genT T, Same.commit gen t) - handle Same.SAME => Abs (x, T, gen t)) - | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u); - in gen tm end; +fun generalize_same (tfrees, frees) idx tm = + if Symtab.is_empty tfrees andalso Symtab.is_empty frees then raise Same.SAME + else + let + val genT = generalizeT_same tfrees idx; + fun gen (Free (x, T)) = + if Symtab.defined frees x then + Var (Name.clean_index (x, idx), Same.commit genT T) + else Free (x, genT T) + | gen (Var (xi, T)) = Var (xi, genT T) + | gen (Const (c, T)) = Const (c, genT T) + | gen (Bound _) = raise Same.SAME + | gen (Abs (x, T, t)) = + (Abs (x, genT T, Same.commit gen t) + handle Same.SAME => Abs (x, T, gen t)) + | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u); + in gen tm end; fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty; fun generalize names i tm = Same.commit (generalize_same names i) tm; diff -r bf9871795aeb -r 10455384a3e5 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/thm.ML Thu Aug 26 16:24:48 2021 +0200 @@ -151,9 +151,9 @@ val equal_elim: thm -> thm -> thm val solve_constraints: thm -> thm val flexflex_rule: Proof.context option -> thm -> thm Seq.seq - val generalize: string list * string list -> int -> thm -> thm - val generalize_cterm: string list * string list -> int -> cterm -> cterm - val generalize_ctyp: string list -> int -> ctyp -> ctyp + val generalize: Symtab.set * Symtab.set -> int -> thm -> thm + val generalize_cterm: Symtab.set * Symtab.set -> int -> cterm -> cterm + val generalize_ctyp: Symtab.set -> int -> ctyp -> ctyp val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> @@ -1542,56 +1542,57 @@ A[?'a/'a, ?x/x, ...] *) -fun generalize ([], []) _ th = th - | generalize (tfrees, frees) idx th = - let - val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; - val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); +fun generalize (tfrees, frees) idx th = + if Symtab.is_empty tfrees andalso Symtab.is_empty frees then th + else + let + val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th; + val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); - val bad_type = - if null tfrees then K false - else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false); - fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x - | bad_term (Var (_, T)) = bad_type T - | bad_term (Const (_, T)) = bad_type T - | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t - | bad_term (t $ u) = bad_term t orelse bad_term u - | bad_term (Bound _) = false; - val _ = exists bad_term hyps andalso - raise THM ("generalize: variable free in assumptions", 0, [th]); + val bad_type = + if Symtab.is_empty tfrees then K false + else Term.exists_subtype (fn TFree (a, _) => Symtab.defined tfrees a | _ => false); + fun bad_term (Free (x, T)) = bad_type T orelse Symtab.defined frees x + | bad_term (Var (_, T)) = bad_type T + | bad_term (Const (_, T)) = bad_type T + | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t + | bad_term (t $ u) = bad_term t orelse bad_term u + | bad_term (Bound _) = false; + val _ = exists bad_term hyps andalso + raise THM ("generalize: variable free in assumptions", 0, [th]); - val generalize = Term_Subst.generalize (tfrees, frees) idx; - val prop' = generalize prop; - val tpairs' = map (apply2 generalize) tpairs; - val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); - in - Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, - {cert = cert, - tags = [], - maxidx = maxidx', - constraints = constraints, - shyps = shyps, - hyps = hyps, - tpairs = tpairs', - prop = prop'}) - end; + val generalize = Term_Subst.generalize (tfrees, frees) idx; + val prop' = generalize prop; + val tpairs' = map (apply2 generalize) tpairs; + val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); + in + Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der, + {cert = cert, + tags = [], + maxidx = maxidx', + constraints = constraints, + shyps = shyps, + hyps = hyps, + tpairs = tpairs', + prop = prop'}) + end; -fun generalize_cterm ([], []) _ ct = ct - | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = - if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) - else - Cterm {cert = cert, sorts = sorts, - T = Term_Subst.generalizeT tfrees idx T, - t = Term_Subst.generalize (tfrees, frees) idx t, - maxidx = Int.max (maxidx, idx)}; +fun generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) = + if Symtab.is_empty tfrees andalso Symtab.is_empty frees then ct + else if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct]) + else + Cterm {cert = cert, sorts = sorts, + T = Term_Subst.generalizeT tfrees idx T, + t = Term_Subst.generalize (tfrees, frees) idx t, + maxidx = Int.max (maxidx, idx)}; -fun generalize_ctyp [] _ cT = cT - | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) = - if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) - else - Ctyp {cert = cert, sorts = sorts, - T = Term_Subst.generalizeT tfrees idx T, - maxidx = Int.max (maxidx, idx)}; +fun generalize_ctyp tfrees idx (cT as Ctyp {cert, T, maxidx, sorts}) = + if Symtab.is_empty tfrees then cT + else if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", []) + else + Ctyp {cert = cert, sorts = sorts, + T = Term_Subst.generalizeT tfrees idx T, + maxidx = Int.max (maxidx, idx)}; (*Instantiation of schematic variables diff -r bf9871795aeb -r 10455384a3e5 src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Aug 26 13:40:49 2021 +0200 +++ b/src/Pure/variable.ML Thu Aug 26 16:24:48 2021 +0200 @@ -516,14 +516,14 @@ val still_fixed = not o is_newly_fixed inner outer; val gen_fixes = - Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y) - (fixes_of inner) []; + Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Symtab.insert_set y) + (fixes_of inner) Symtab.empty; val type_occs_inner = type_occs_of inner; fun gen_fixesT ts = Symtab.fold (fn (a, xs) => if declared_outer a orelse exists still_fixed xs - then I else cons a) (fold decl_type_occs ts type_occs_inner) []; + then I else Symtab.insert_set a) (fold decl_type_occs ts type_occs_inner) Symtab.empty; in (gen_fixesT, gen_fixes) end; fun exportT_inst inner outer = #1 (export_inst inner outer); @@ -534,7 +534,7 @@ val maxidx = maxidx_of outer; in fn ts => ts |> map - (Term_Subst.generalize (mk_tfrees ts, []) + (Term_Subst.generalize (mk_tfrees ts, Symtab.empty) (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) end; @@ -565,7 +565,7 @@ val idx = fold Thm.maxidx_thm ths maxidx + 1; in map (Thm.generalize (tfrees, frees) idx) ths end; -fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer); +fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer); fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); fun export_morphism inner outer = @@ -728,13 +728,15 @@ val ctxt' = fold declare_term ts ctxt; val occs = type_occs_of ctxt; val occs' = type_occs_of ctxt'; - val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' []; + val types = + Symtab.fold (fn (a, _) => + if Symtab.defined occs a then I else Symtab.insert_set a) occs' Symtab.empty; val idx = maxidx_of ctxt' + 1; val Ts' = (fold o fold_types o fold_atyps) (fn T as TFree _ => (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I) | _ => I) ts []; - val ts' = map (Term_Subst.generalize (types, []) idx) ts; + val ts' = map (Term_Subst.generalize (types, Symtab.empty) idx) ts; in (rev Ts', ts') end; fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);