src/Pure/sign.ML
changeset 28863 32e83a854e5e
parent 28861 f53abb0733ee
child 28941 128459bd72d2
     1.1 --- a/src/Pure/sign.ML	Thu Nov 20 14:55:28 2008 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 20 19:06:02 2008 +0100
     1.3 @@ -15,8 +15,6 @@
     1.4      consts: Consts.T}
     1.5    val naming_of: theory -> NameSpace.naming
     1.6    val base_name: string -> bstring
     1.7 -  val name_decl: (string * 'a -> theory -> 'b * theory)
     1.8 -    -> Name.binding * 'a -> theory -> (string * 'b) * theory
     1.9    val full_name: theory -> bstring -> string
    1.10    val full_binding: theory -> Name.binding -> string
    1.11    val full_name_path: theory -> string -> bstring -> string
    1.12 @@ -191,19 +189,6 @@
    1.13  val naming_of = #naming o rep_sg;
    1.14  val base_name = NameSpace.base;
    1.15  
    1.16 -fun name_decl decl (b, x) thy =
    1.17 -  let
    1.18 -    val naming = naming_of thy;
    1.19 -    val (naming', name) = Name.namify naming b;
    1.20 -  in
    1.21 -    thy
    1.22 -    |> map_naming (K naming')
    1.23 -    |> decl (Name.name_of b, x)
    1.24 -    |>> pair name
    1.25 -    ||> map_naming (K naming)
    1.26 -  end;
    1.27 -
    1.28 -val namify = Name.namify o naming_of;
    1.29  val full_name = NameSpace.full o naming_of;
    1.30  val full_binding = NameSpace.full_binding o naming_of;
    1.31  fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));