src/Pure/sign.ML
changeset 30280 eb98b49ef835
parent 30242 aea5d7fa7ef5
child 30343 79f022df8527
--- a/src/Pure/sign.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/sign.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -14,7 +14,6 @@
     consts: Consts.T}
   val naming_of: theory -> NameSpace.naming
   val full_name: theory -> binding -> string
-  val base_name: string -> bstring
   val full_bname: theory -> bstring -> string
   val full_bname_path: theory -> string -> bstring -> string
   val syn_of: theory -> Syntax.syntax
@@ -185,7 +184,6 @@
 (* naming *)
 
 val naming_of = #naming o rep_sg;
-val base_name = NameSpace.base;
 
 val full_name = NameSpace.full_name o naming_of;
 fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;