# HG changeset patch
# User wenzelm
# Date 1717839158 -7200
# Node ID f38771b2df1ccbc8a1211ea9edcb52329a155665
# Parent  a1162cbda70cf5b4892b7eee837a92c17425da56
tuned structure;

diff -r a1162cbda70c -r f38771b2df1c src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Sat Jun 08 11:23:40 2024 +0200
+++ b/src/Pure/thm_name.ML	Sat Jun 08 11:32:38 2024 +0200
@@ -15,17 +15,21 @@
   structure Table: TABLE
   val empty: T
   val is_empty: T -> bool
-  val print: T -> string
-  val short: T -> string
+
   type P = T * Position.T
   val none: P
   val list: string * Position.T -> 'a list -> (P * 'a) list
   val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
+
+  val print: T -> string
+  val short: T -> string
 end;
 
 structure Thm_Name: THM_NAME =
 struct
 
+(* type T *)
+
 type T = string * int;
 val ord = prod_ord string_ord int_ord;
 
@@ -35,14 +39,8 @@
 val empty: T = ("", 0);
 fun is_empty ((a, _): T) = a = "";
 
-fun print (name, index) =
-  if name = "" orelse index = 0 then name
-  else name ^ enclose "(" ")" (string_of_int index);
 
-fun short (name, index) =
-  if name = "" orelse index = 0 then name
-  else name ^ "_" ^ string_of_int index;
-
+(* type P *)
 
 type P = T * Position.T;
 
@@ -54,4 +52,15 @@
 
 fun expr name = burrow_fst (burrow (list name));
 
+
+(* output *)
+
+fun print (name, index) =
+  if name = "" orelse index = 0 then name
+  else name ^ enclose "(" ")" (string_of_int index);
+
+fun short (name, index) =
+  if name = "" orelse index = 0 then name
+  else name ^ "_" ^ string_of_int index;
+
 end;