--- a/src/Pure/consts.ML Sun Oct 25 12:27:21 2009 +0100
+++ b/src/Pure/consts.ML Sun Oct 25 13:18:35 2009 +0100
@@ -20,6 +20,7 @@
val is_monomorphic: T -> string -> bool (*exception TYPE*)
val the_constraint: T -> string -> typ (*exception TYPE*)
val space_of: T -> Name_Space.T
+ val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
val extern: T -> string -> xstring
val extern_early: T -> string -> xstring
@@ -123,6 +124,8 @@
fun space_of (Consts {decls = (space, _), ...}) = space;
+val is_concealed = Name_Space.is_concealed o space_of;
+
val intern = Name_Space.intern o space_of;
val extern = Name_Space.extern o space_of;