# HG changeset patch
# User wenzelm
# Date 1681559526 -7200
# Node ID 64533f3818a467dce64c49454419fc819e404e03
# Parent  5286dae99de312945f897666988068b32d950fad
tuned signature;

diff -r 5286dae99de3 -r 64533f3818a4 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Sat Apr 15 13:51:38 2023 +0200
+++ b/src/Pure/General/long_name.ML	Sat Apr 15 13:52:06 2023 +0200
@@ -8,6 +8,7 @@
 sig
   val separator: string
   val is_qualified: string -> bool
+  val count: string -> int
   val hidden: string -> string
   val is_hidden: string -> bool
   val dest_hidden: string -> string option
@@ -16,7 +17,6 @@
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
-  val qualification: string -> int
   val qualify: string -> string -> string
   val qualifier: string -> string
   val base_name: string -> string
@@ -44,6 +44,9 @@
 
 fun is_qualified name = String.member name separator_char;
 
+fun count "" = 0
+  | count name = String.fold (fn c => c = separator_char ? Integer.add 1) name 1;
+
 val hidden_prefix = "??."
 val hidden = prefix hidden_prefix;
 val is_hidden = String.isPrefix hidden_prefix;
@@ -59,9 +62,6 @@
   | append "" name2 = name2
   | append name1 name2 = name1 ^ separator ^ name2;
 
-fun qualification "" = 0
-  | qualification name = fold_string (fn s => s = separator ? Integer.add 1) name 1;
-
 fun qualify qual name =
   if qual = "" orelse name = "" then name
   else qual ^ separator ^ name;
diff -r 5286dae99de3 -r 64533f3818a4 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Apr 15 13:51:38 2023 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 15 13:52:06 2023 +0200
@@ -283,7 +283,7 @@
           EQUAL =>
             (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
               EQUAL =>
-                (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
+                (case int_ord (apply2 Long_Name.count (xname1, xname2)) of
                   EQUAL => string_ord (xname1, xname2)
                 | ord => ord)
             | ord => ord)
diff -r 5286dae99de3 -r 64533f3818a4 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Apr 15 13:51:38 2023 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 15 13:52:06 2023 +0200
@@ -335,7 +335,7 @@
 
 val index_ord = option_ord (K EQUAL);
 val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
-val qual_ord = int_ord o apply2 Long_Name.qualification;
+val qual_ord = int_ord o apply2 Long_Name.count;
 val txt_ord = int_ord o apply2 size;
 
 fun nicer_name ((a, x), i) ((b, y), j) =