# HG changeset patch # User wenzelm # Date 1732836303 -3600 # Node ID 01f2936ec85e00d5a112cf42a5ff6424bf53e30e # Parent 7b85ebdab12cfae408991b55a2e010b9c89a0fdc clarified signature: more uniform; diff -r 7b85ebdab12c -r 01f2936ec85e src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Thu Nov 28 19:35:30 2024 +0100 +++ b/src/HOL/Inductive.thy Fri Nov 29 00:25:03 2024 +0100 @@ -532,7 +532,7 @@ let fun fun_tr ctxt [cs] = let - val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context))); + val x = Syntax.free (fst (Name.variant "x" (Term.declare_free_names cs Name.context))); val ft = Case_Translation.case_tr true ctxt [x, cs]; in lambda x ft end in [(\<^syntax_const>\_lam_pats_syntax\, fun_tr)] end diff -r 7b85ebdab12c -r 01f2936ec85e src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Nov 29 00:25:03 2024 +0100 @@ -161,7 +161,7 @@ | replace_dummies t used = (t, used); fun dest_case1 (t as Const (\<^syntax_const>\_case1\, _) $ l $ r) = - let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context) in + let val (l', _) = replace_dummies l (Term.declare_free_names t Name.context) in abs_pat l' [] (Syntax.const \<^const_syntax>\case_elem\ $ Term_Position.strip_positions l' $ r) end @@ -198,7 +198,7 @@ fun mk_clauses (Const (\<^const_syntax>\case_nil\, _)) = [] | mk_clauses (Const (\<^const_syntax>\case_cons\, _) $ t $ u) = - mk_clause t [] (Term.declare_term_frees t Name.context) :: mk_clauses u + mk_clause t [] (Term.declare_free_names t Name.context) :: mk_clauses u | mk_clauses _ = raise Match; in list_comb (Syntax.const \<^syntax_const>\_case_syntax\ $ x $ @@ -248,7 +248,7 @@ completion.*) fun add_row_used ((prfx, pats), (tm, _)) = - fold Term.declare_term_frees (tm :: pats @ map Free prfx); + fold Term.declare_free_names (tm :: pats @ map Free prfx); (*try to preserve names given by user*) fun default_name "" (Free (name', _)) = name' @@ -307,7 +307,7 @@ val (xs, _) = fold_map Name.variant (replicate (length ps) "x") - (fold Term.declare_term_frees gvars used'); + (fold Term.declare_free_names gvars used'); in [((prfx, gvars @ map Free (xs ~~ Ts)), (Const (\<^const_name>\undefined\, res_ty), ~1))] @@ -361,7 +361,7 @@ | SOME (case_comb, constructors) => let val pty = body_type cT; - val used' = fold Term.declare_term_frees us used; + val used' = fold Term.declare_free_names us used; val nrows = maps (expand constructors used' pty) rows; val subproblems = partition used' constructors pty range_ty nrows; val (pat_rect, dtrees) = @@ -440,7 +440,7 @@ fun decode_cases (Const (\<^const_name>\case_nil\, _)) = [] | decode_cases (Const (\<^const_name>\case_cons\, _) $ t $ u) = - decode_clause t [] (Term.declare_term_frees t Name.context) :: + decode_clause t [] (Term.declare_free_names t Name.context) :: decode_cases u | decode_cases _ = case_error "decode_cases"; @@ -562,7 +562,7 @@ | encode_case _ _ = case_error "encode_case"; fun strip_case' ctxt d (pat, rhs) = - (case dest_case ctxt d (Term.declare_term_frees pat Name.context) rhs of + (case dest_case ctxt d (Term.declare_free_names pat Name.context) rhs of SOME (exp as Free _, clauses) => if Term.exists_subterm (curry (op aconv) exp) pat andalso not (exists (fn (_, rhs') => diff -r 7b85ebdab12c -r 01f2936ec85e src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/Pure/Proof/proof_checker.ML Fri Nov 29 00:25:03 2024 +0100 @@ -76,7 +76,7 @@ fn prf => let val prf_names = - Name.build_context (prf |> Proofterm.fold_proof_terms Term.declare_term_frees); + Name.build_context (prf |> Proofterm.fold_proof_terms Term.declare_free_names); fun thm_of_atom thm Ts = let diff -r 7b85ebdab12c -r 01f2936ec85e src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Nov 29 00:25:03 2024 +0100 @@ -212,7 +212,7 @@ fun rew_term Ts t = let val frees = - map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts); + map Free (Name.invent (Term.declare_free_names t Name.context) "xa" (length Ts) ~~ Ts); val t' = r (subst_bounds (frees, t)); fun strip [] t = t | strip (_ :: xs) (Abs (_, _, t)) = strip xs t; diff -r 7b85ebdab12c -r 01f2936ec85e src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/Pure/more_thm.ML Fri Nov 29 00:25:03 2024 +0100 @@ -349,7 +349,7 @@ val used_frees = Name.build_context o - Thm.fold_terms {hyps = true} Term.declare_term_frees; + Thm.fold_terms {hyps = true} Term.declare_free_names; fun used_vars i = Name.build_context o diff -r 7b85ebdab12c -r 01f2936ec85e src/Pure/term.ML --- a/src/Pure/term.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/Pure/term.ML Fri Nov 29 00:25:03 2024 +0100 @@ -151,10 +151,11 @@ val add_frees: term -> (string * typ) list -> (string * typ) list val add_const_names: term -> string list -> string list val add_consts: term -> (string * typ) list -> (string * typ) list + val declare_tfree_namesT: typ -> Name.context -> Name.context + val declare_tfree_names: term -> Name.context -> Name.context + val declare_free_names: term -> Name.context -> Name.context val hidden_polymorphism: term -> (indexname * sort) list - val declare_typ_names: typ -> Name.context -> Name.context val declare_term_names: term -> Name.context -> Name.context - val declare_term_frees: term -> Name.context -> Name.context val variant_frees: term -> (string * 'a) list -> (string * 'a) list val smash_sortsT_same: sort -> typ Same.operation val smash_sortsT: sort -> typ -> typ @@ -573,6 +574,9 @@ val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I); val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I); val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I); +val declare_tfree_namesT = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); +val declare_tfree_names = fold_types declare_tfree_namesT; +val declare_free_names = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); (*extra type variables in a term, not covered by its type*) fun hidden_polymorphism t = @@ -586,16 +590,12 @@ (* renaming variables *) -val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); - fun declare_term_names tm = fold_aterms (fn Const (a, _) => Name.declare (Long_Name.base_name a) | Free (a, _) => Name.declare a | _ => I) tm #> - fold_types declare_typ_names tm; - -val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); + declare_tfree_names tm; fun variant_frees t frees = fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~ @@ -812,7 +812,7 @@ of bound variables and implicit eta-expansion*) fun strip_abs_eta k t = let - val used = fold_aterms declare_term_frees t Name.context; + val used = fold_aterms declare_free_names t Name.context; fun strip_abs t (0, used) = (([], t), (0, used)) | strip_abs (Abs (v, T, t)) (k, used) = let @@ -1074,7 +1074,7 @@ Abs (x, T, b) => if used_free x b then let - val used = Name.build_context (declare_term_frees b); + val used = Name.build_context (declare_free_names b); val x' = #1 (Name.variant x used); in subst_abs (x', T) b end else subst_abs (x, T) b diff -r 7b85ebdab12c -r 01f2936ec85e src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/Pure/type_infer.ML Fri Nov 29 00:25:03 2024 +0100 @@ -115,7 +115,7 @@ in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end else (inst, used); val params = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set; - val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt); + val used = fold Term.declare_tfree_names ts (Variable.names_of ctxt); val (inst, _) = fold subst_param params (TVars.empty, used); in (Same.commit o Same.map o Term.map_types_same) (Term_Subst.instantiateT_same inst) ts end; diff -r 7b85ebdab12c -r 01f2936ec85e src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/Pure/variable.ML Fri Nov 29 00:25:03 2024 +0100 @@ -214,12 +214,12 @@ (* names *) fun declare_type_names t = - map_names (fold_types Term.declare_typ_names t) #> + map_names (Term.declare_tfree_names t) #> map_maxidx (fold_types Term.maxidx_typ t); fun declare_names t = declare_type_names t #> - map_names (Term.declare_term_frees t) #> + map_names (Term.declare_free_names t) #> map_maxidx (Term.maxidx_term t);