# HG changeset patch
# User wenzelm
# Date 1394442266 -3600
# Node ID f252a315c26e459bf9c5263e88b06a79380c0546
# Parent  8c9ab5d91d5a3c5d011c8d52cabda434b570c093
more direct Long_Name.qualification;

diff -r 8c9ab5d91d5a -r f252a315c26e src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Mon Mar 10 09:54:01 2014 +0100
+++ b/src/Pure/General/long_name.ML	Mon Mar 10 10:04:26 2014 +0100
@@ -13,6 +13,7 @@
   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
@@ -35,6 +36,9 @@
   | 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 8c9ab5d91d5a -r f252a315c26e src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Mar 10 09:54:01 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Mar 10 10:04:26 2014 +0100
@@ -330,7 +330,7 @@
 
 val index_ord = option_ord (K EQUAL);
 val hidden_ord = bool_ord o pairself Long_Name.is_hidden;
-val qual_ord = int_ord o pairself (length o Long_Name.explode);
+val qual_ord = int_ord o pairself Long_Name.qualification;
 val txt_ord = int_ord o pairself size;
 
 fun nicer_name (x, i) (y, j) =