--- a/src/Doc/Implementation/Logic.thy Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy Thu Aug 26 14:45:19 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>\<open>Thm.generalize\<close>~\<open>(\<^vec>\<alpha>, \<^vec>x)\<close> corresponds to the
\<open>generalize\<close> 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>\<open>Thm.instantiate\<close>~\<open>(\<^vec>\<alpha>\<^sub>s, \<^vec>x\<^sub>\<tau>)\<close> corresponds to the
\<open>instantiate\<close> rules of \figref{fig:subst-rules}. Type variables are
--- a/src/HOL/Eisbach/match_method.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML Thu Aug 26 14:45:19 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;
--- a/src/HOL/Library/cconv.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Library/cconv.ML Thu Aug 26 14:45:19 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
--- a/src/HOL/Library/code_lazy.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Thu Aug 26 14:45:19 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>\<open>Pure.dummy_pattern\<close>, 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
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Aug 26 14:45:19 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 =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Aug 26 14:45:19 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);
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Aug 26 14:45:19 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;
--- a/src/HOL/Tools/Function/induction_schema.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Thu Aug 26 14:45:19 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
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 26 14:45:19 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)
--- a/src/HOL/Tools/Transfer/transfer.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Thu Aug 26 14:45:19 2021 +0200
@@ -575,7 +575,7 @@
((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), 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>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), 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
--- a/src/Pure/Isar/local_defs.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/Isar/local_defs.ML Thu Aug 26 14:45:19 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);
--- a/src/Pure/drule.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/drule.ML Thu Aug 26 14:45:19 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
--- a/src/Pure/goal.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/goal.ML Thu Aug 26 14:45:19 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 =
--- a/src/Pure/more_thm.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/more_thm.ML Thu Aug 26 14:45:19 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;
--- a/src/Pure/proofterm.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/proofterm.ML Thu Aug 26 14:45:19 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
--- a/src/Pure/term_subst.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/term_subst.ML Thu Aug 26 14:45:19 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;
--- a/src/Pure/thm.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/thm.ML Thu Aug 26 14:45:19 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
--- a/src/Pure/variable.ML Wed Aug 25 22:17:38 2021 +0200
+++ b/src/Pure/variable.ML Thu Aug 26 14:45:19 2021 +0200
@@ -534,7 +534,7 @@
val maxidx = maxidx_of outer;
in
fn ts => ts |> map
- (Term_Subst.generalize (mk_tfrees ts, [])
+ (Term_Subst.generalize (Symtab.make_set (mk_tfrees ts), Symtab.empty)
(fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1))
end;
@@ -544,17 +544,17 @@
val maxidx = maxidx_of outer;
in
fn ts => ts |> map
- (Term_Subst.generalize (mk_tfrees ts, tfrees)
+ (Term_Subst.generalize (Symtab.make_set (mk_tfrees ts), Symtab.make_set tfrees)
(fold Term.maxidx_term ts maxidx + 1))
end;
fun export_prf inner outer prf =
let
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
- val tfrees = mk_tfrees [];
+ val tfrees = Symtab.make_set (mk_tfrees []);
val maxidx = maxidx_of outer;
val idx = Proofterm.maxidx_proof prf maxidx + 1;
- val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
+ val gen_term = Term_Subst.generalize_same (tfrees, Symtab.make_set frees) idx;
val gen_typ = Term_Subst.generalizeT_same tfrees idx;
in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
@@ -563,7 +563,7 @@
let
val tfrees = mk_tfrees (map Thm.full_prop_of ths);
val idx = fold Thm.maxidx_thm ths maxidx + 1;
- in map (Thm.generalize (tfrees, frees) idx) ths end;
+ in map (Thm.generalize (Symtab.make_set tfrees, Symtab.make_set frees) idx) ths end;
fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer);
fun export inner outer = gen_export (export_inst inner outer) (maxidx_of 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);