1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Mar 17 23:50:47 2012 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Mar 17 23:55:03 2012 +0100
     1.3 @@ -141,6 +141,7 @@
     1.4      Context.generic -> Context.generic
     1.5    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     1.6      Context.generic -> Context.generic
     1.7 +  val target_naming_of: Context.generic -> Name_Space.naming
     1.8    val class_alias: binding -> class -> Proof.context -> Proof.context
     1.9    val type_alias: binding -> string -> Proof.context -> Proof.context
    1.10    val const_alias: binding -> string -> Proof.context -> Proof.context
    1.11 @@ -992,6 +993,11 @@
    1.12  end;
    1.13  
    1.14  
    1.15 +(* naming *)
    1.16 +
    1.17 +val target_naming_of = Context.cases Sign.naming_of naming_of;
    1.18 +
    1.19 +
    1.20  (* aliases *)
    1.21  
    1.22  fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;