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