--- a/src/Pure/General/name_space.ML Mon Mar 19 19:49:54 2012 +0100
+++ b/src/Pure/General/name_space.ML Mon Mar 19 20:32:57 2012 +0100
@@ -49,6 +49,7 @@
val local_naming: naming
val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
+ val base_name: binding -> string
val alias: naming -> binding -> string -> T -> T
val naming_of: Context.generic -> naming
val map_naming: (naming -> naming) -> Context.generic -> Context.generic
@@ -314,6 +315,8 @@
fun full_name naming =
name_spec naming #> #2 #> map #1 #> Long_Name.implode;
+val base_name = full_name default_naming #> Long_Name.base_name;
+
(* accesses *)