src/Pure/Isar/proof_context.ML
changeset 28792 1d80cee865de
parent 28417 74e580c6f2b5
child 28856 5e009a80fe6d
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Nov 14 08:50:09 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Nov 14 08:50:10 2008 +0100
     1.3 @@ -23,6 +23,8 @@
     1.4    val abbrev_mode: Proof.context -> bool
     1.5    val set_stmt: bool -> Proof.context -> Proof.context
     1.6    val naming_of: Proof.context -> NameSpace.naming
     1.7 +  val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context)
     1.8 +    -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context
     1.9    val full_name: Proof.context -> bstring -> string
    1.10    val consts_of: Proof.context -> Consts.T
    1.11    val const_syntax_name: Proof.context -> string -> string
    1.12 @@ -245,6 +247,19 @@
    1.13    map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
    1.14  
    1.15  val naming_of = #naming o rep_context;
    1.16 +
    1.17 +fun name_decl decl (binding, x) ctxt =
    1.18 +  let
    1.19 +    val naming = naming_of ctxt;
    1.20 +    val (naming', name) = Name.namify naming binding;
    1.21 +  in
    1.22 +    ctxt
    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 full_name = NameSpace.full o naming_of;
    1.30  
    1.31  val syntax_of = #syntax o rep_context;