# HG changeset patch
# User wenzelm
# Date 1193670824 -3600
# Node ID e638164593bf67a51e31196c652e726a120bdb3e
# Parent  6d4d26e878f4044f5e9f9c47068a1b6ae29ad34c
export is_hidden;

diff -r 6d4d26e878f4 -r e638164593bf src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Oct 29 16:13:43 2007 +0100
+++ b/src/Pure/General/name_space.ML	Mon Oct 29 16:13:44 2007 +0100
@@ -20,6 +20,7 @@
 sig
   include BASIC_NAME_SPACE
   val hidden: string -> string
+  val is_hidden: string -> bool
   val separator: string                 (*single char*)
   val is_qualified: string -> bool
   val implode: string list -> string