# HG changeset patch
# User wenzelm
# Date 1703706015 -3600
# Node ID b275e3379024f0f7875547e9e635947b7d3abe2e
# Parent  06ab0a304f29e2eaac04c00cfae170266a81aa67
tuned signature;

diff -r 06ab0a304f29 -r b275e3379024 src/Pure/Isar/generic_target.ML
--- 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
diff -r 06ab0a304f29 -r b275e3379024 src/Pure/global_theory.ML
--- 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 =>
diff -r 06ab0a304f29 -r b275e3379024 src/Pure/thm_name.ML
--- 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);
 
diff -r 06ab0a304f29 -r b275e3379024 src/Pure/thm_name.scala
--- 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
 }