--- a/src/Pure/Isar/generic_target.ML Wed Dec 27 20:31:01 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML Wed Dec 27 20:40:15 2023 +0100
@@ -296,8 +296,8 @@
local
-val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.flatten;
-val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.flatten;
+val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.short;
+val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.short;
fun thm_def (name, pos) thm lthy =
if #1 name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
--- a/src/Pure/global_theory.ML Wed Dec 27 20:31:01 2023 +0100
+++ b/src/Pure/global_theory.ML Wed Dec 27 20:40:15 2023 +0100
@@ -252,14 +252,14 @@
end;
-fun name_thm_flatten name_flags name =
- name_thm name_flags (Thm_Name.flatten name);
+fun name_thm_short name_flags name =
+ name_thm name_flags (Thm_Name.short name);
fun name_thms name_flags name_pos thms =
- Thm_Name.list name_pos thms |> map (uncurry (name_thm_flatten name_flags));
+ Thm_Name.list name_pos thms |> map (uncurry (name_thm_short name_flags));
fun name_facts name_flags name_pos facts =
- Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm_flatten name_flags));
+ Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm_short name_flags));
(* store theorems and proofs *)
@@ -309,7 +309,7 @@
val named_facts = Thm_Name.expr name facts;
val unnamed = #1 name = "";
- val name_thm1 = if unnamed then #2 else uncurry (name_thm_flatten name_flags1);
+ val name_thm1 = if unnamed then #2 else uncurry (name_thm_short name_flags1);
val app_facts =
fold_maps (fn (named_thms, atts) => fn thy =>
--- a/src/Pure/thm_name.ML Wed Dec 27 20:31:01 2023 +0100
+++ b/src/Pure/thm_name.ML Wed Dec 27 20:40:15 2023 +0100
@@ -12,7 +12,7 @@
type T = string * int
val ord: T ord
val print: T -> string
- val flatten: T * Position.T -> string * Position.T
+ val short: T * Position.T -> string * Position.T
val list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
val expr: string * Position.T -> ('a list * 'b) list -> (((T * Position.T) * 'a) list * 'b) list
end;
@@ -27,7 +27,7 @@
if name = "" orelse index = 0 then name
else name ^ enclose "(" ")" (string_of_int index);
-fun flatten ((name, index), pos) =
+fun short ((name, index), pos: Position.T) =
if name = "" orelse index = 0 then (name, pos)
else (name ^ "_" ^ string_of_int index, pos);
--- a/src/Pure/thm_name.scala Wed Dec 27 20:31:01 2023 +0100
+++ b/src/Pure/thm_name.scala Wed Dec 27 20:40:15 2023 +0100
@@ -35,7 +35,7 @@
if (name == "" || index == 0) name
else name + "(" + index + ")"
- def flatten: String =
+ def short: String =
if (name == "" || index == 0) name
else name + "_" + index
}