# HG changeset patch # User wenzelm # Date 1733058107 -3600 # Node ID 1bfad73ab115f6bfcba22a392a4034f4350559c8 # Parent 878bc24681d90ae6f92b01a4262d53b846fb6266 clarified signature: more operations; diff -r 878bc24681d9 -r 1bfad73ab115 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/HOL/Import/import_rule.ML Sun Dec 01 14:01:47 2024 +0100 @@ -335,7 +335,7 @@ val thm = Drule.export_without_context_open thm val tvs = Term.add_tvars (Thm.prop_of thm) [] val tns = map (fn (_, _) => "'") tvs - val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt)) + val nms = Name.variants (Variable.names_of ctxt) tns val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs)) val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm in diff -r 878bc24681d9 -r 1bfad73ab115 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Sun Dec 01 14:01:47 2024 +0100 @@ -34,7 +34,7 @@ let val (vs, Ts) = split_list (strip_qnt_vars \<^const_name>\Pure.all\ t); val body = strip_qnt_body \<^const_name>\Pure.all\ t; - val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms + val vs' = vs |> Name.variants (Name.make_context (fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) body [])) in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end; diff -r 878bc24681d9 -r 1bfad73ab115 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Sun Dec 01 14:01:47 2024 +0100 @@ -260,7 +260,7 @@ let val T = dest_Const_type c; val Ts = binder_types T; - val (names, _) = fold_map Name.variant (make_tnames Ts) used; + val names = Name.variants used (make_tnames Ts); val ty = body_type T; val ty_theta = Type.raw_match (ty, colty) Vartab.empty handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1); @@ -304,10 +304,9 @@ then let val Ts = map fastype_of ps; - val (xs, _) = - fold_map Name.variant - (replicate (length ps) "x") - (fold Term.declare_free_names gvars used'); + val xs = + Name.variants (fold Term.declare_free_names gvars used') + (replicate (length ps) "x"); in [((prfx, gvars @ map Free (xs ~~ Ts)), (Const (\<^const_name>\undefined\, res_ty), ~1))] diff -r 878bc24681d9 -r 1bfad73ab115 src/HOL/Tools/Old_Datatype/old_primrec.ML --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Sun Dec 01 14:01:47 2024 +0100 @@ -38,7 +38,7 @@ let val (vs, Ts) = split_list (strip_qnt_vars \<^const_name>\Pure.all\ spec); val body = strip_qnt_body \<^const_name>\Pure.all\ spec; - val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms + val vs' = vs |> Name.variants (Name.make_context (fold_aterms (fn Free (v, _) => insert (op =) v | _ => I) body [])); val eqn = curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body; val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn) diff -r 878bc24681d9 -r 1bfad73ab115 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/Pure/Isar/code.ML Sun Dec 01 14:01:47 2024 +0100 @@ -1465,8 +1465,7 @@ fun case_cong thy case_const (num_args, (pos, _)) = let - val ([x, y], ctxt) = fold_map Name.variant ["A", "A'"] Name.context; - val (zs, _) = fold_map Name.variant (replicate (num_args - 1) "") ctxt; + val x :: y :: zs = Name.variants Name.context ("A" :: "A'" :: replicate (num_args - 1) ""); val (ws, vs) = chop pos zs; val T = devarify (const_typ thy case_const); val Ts = binder_types T; diff -r 878bc24681d9 -r 1bfad73ab115 src/Pure/name.ML --- a/src/Pure/name.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/Pure/name.ML Sun Dec 01 14:01:47 2024 +0100 @@ -41,6 +41,7 @@ val variant_bound: string -> context -> string * context val variant_names: context -> (string * 'a) list -> (string * 'a) list val variant_names_build: (context -> context) -> (string * 'a) list -> (string * 'a) list + val variants: context -> string list -> string list val variant_list: string list -> string list -> string list val enforce_case: bool -> string -> string val desymbolize: bool option -> string -> string @@ -177,7 +178,8 @@ fun variant_names ctxt xs = #1 (fold_map (variant o fst) xs ctxt) ~~ map snd xs; fun variant_names_build f xs = variant_names (build_context f) xs; -fun variant_list used names = #1 (make_context used |> fold_map variant names); +fun variants ctxt xs = #1 (fold_map variant xs ctxt); +val variant_list = variants o make_context; (* names conforming to typical requirements of identifiers in the world outside *) diff -r 878bc24681d9 -r 1bfad73ab115 src/Pure/type.ML --- a/src/Pure/type.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/Pure/type.ML Sun Dec 01 14:01:47 2024 +0100 @@ -346,7 +346,7 @@ build (t |> (Term.fold_types o Term.fold_atyps) (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I)); val used = Name.build_context (t |> Term.declare_tvar_names (K true)); - val ys = #1 (fold_map Name.variant (map #1 xs) used); + val ys = Name.variants used (map #1 xs); in map2 (fn (a, S) => fn b => ((a, S), ((b, 0), S))) xs ys end; fun varify_global fixed t = diff -r 878bc24681d9 -r 1bfad73ab115 src/Pure/variable.ML --- a/src/Pure/variable.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/Pure/variable.ML Sun Dec 01 14:01:47 2024 +0100 @@ -327,7 +327,7 @@ | bounds => let val names = Term.declare_term_names t (names_of ctxt); - val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names)); + 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)) in [subst T, subst (Type_Annotation.ignore_type T)] end; diff -r 878bc24681d9 -r 1bfad73ab115 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/Tools/Code/code_printer.ML Sun Dec 01 14:01:47 2024 +0100 @@ -188,7 +188,7 @@ val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE); val x = singleton (Name.variant_list (map_filter I fished1)) "x"; val fished2 = map_index (fillup_param x) fished1; - val (fished3, _) = fold_map Name.variant fished2 Name.context; + val fished3 = Name.variants Name.context fished2; val vars' = intro_vars fished3 vars; in map (lookup_var vars') fished3 end; diff -r 878bc24681d9 -r 1bfad73ab115 src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Sat Nov 30 23:30:36 2024 +0100 +++ b/src/Tools/IsaPlanner/isand.ML Sun Dec 01 14:01:47 2024 +0100 @@ -57,7 +57,7 @@ val names = Variable.names_of ctxt |> fold (fn t => Term.declare_free_names t #> Term.declare_var_names (K true) t) ts; - in fst (fold_map Name.variant xs names) end; + in Name.variants names xs end; (* fix parameters of a subgoal "i", as free variables, and create an exporting function that will use the result of this proved goal to