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;