src/Pure/sign.ML
changeset 28792 1d80cee865de
parent 28111 ea22fd4685fb
child 28861 f53abb0733ee
     1.1 --- a/src/Pure/sign.ML	Fri Nov 14 08:50:09 2008 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Nov 14 08:50:10 2008 +0100
     1.3 @@ -15,6 +15,8 @@
     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_name_path: theory -> string -> bstring -> string
    1.11    val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    1.12 @@ -187,6 +189,20 @@
    1.13  
    1.14  val naming_of = #naming o rep_sg;
    1.15  val base_name = NameSpace.base;
    1.16 +
    1.17 +fun name_decl decl (binding, x) thy =
    1.18 +  let
    1.19 +    val naming = naming_of thy;
    1.20 +    val (naming', name) = Name.namify naming binding;
    1.21 +  in
    1.22 +    thy
    1.23 +    |> map_naming (K naming')
    1.24 +    |> decl (Name.name_of binding, x)
    1.25 +    |>> pair name
    1.26 +    ||> map_naming (K naming)
    1.27 +  end;
    1.28 +
    1.29 +val namify = Name.namify o naming_of;
    1.30  val full_name = NameSpace.full o naming_of;
    1.31  fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
    1.32  val declare_name = NameSpace.declare o naming_of;