diff -r 53f13f763d4f -r 32e83a854e5e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Nov 20 14:55:28 2008 +0100
+++ b/src/Pure/sign.ML	Thu Nov 20 19:06:02 2008 +0100
@@ -15,8 +15,6 @@
     consts: Consts.T}
   val naming_of: theory -> NameSpace.naming
   val base_name: string -> bstring
-  val name_decl: (string * 'a -> theory -> 'b * theory)
-    -> Name.binding * 'a -> theory -> (string * 'b) * theory
   val full_name: theory -> bstring -> string
   val full_binding: theory -> Name.binding -> string
   val full_name_path: theory -> string -> bstring -> string
@@ -191,19 +189,6 @@
 val naming_of = #naming o rep_sg;
 val base_name = NameSpace.base;
 
-fun name_decl decl (b, x) thy =
-  let
-    val naming = naming_of thy;
-    val (naming', name) = Name.namify naming b;
-  in
-    thy
-    |> map_naming (K naming')
-    |> decl (Name.name_of b, x)
-    |>> pair name
-    ||> map_naming (K naming)
-  end;
-
-val namify = Name.namify o naming_of;
 val full_name = NameSpace.full o naming_of;
 val full_binding = NameSpace.full_binding o naming_of;
 fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));