--- a/src/Pure/Isar/proof_context.ML Sat Mar 17 23:50:47 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Mar 17 23:55:03 2012 +0100
@@ -141,6 +141,7 @@
Context.generic -> Context.generic
val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
Context.generic -> Context.generic
+ val target_naming_of: Context.generic -> Name_Space.naming
val class_alias: binding -> class -> Proof.context -> Proof.context
val type_alias: binding -> string -> Proof.context -> Proof.context
val const_alias: binding -> string -> Proof.context -> Proof.context
@@ -992,6 +993,11 @@
end;
+(* naming *)
+
+val target_naming_of = Context.cases Sign.naming_of naming_of;
+
+
(* aliases *)
fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;