src/Pure/facts.ML

   val select: ref -> thm list -> thm list
   val selections: string * thm list -> (ref * thm) list
   type T
   val empty: T
   val space_of: T -> Name_Space.T
+  val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a

 struct
 
 (** fact references **)
 
 fun the_single _ [th] : thm = th
-  | the_single name _ = error ("Single theorem expected " ^ quote name);
+  | the_single name _ = error ("Expected singleton fact " ^ quote name);
 
 
 (* datatype interval *)
 
 datatype interval =

 datatype T = Facts of
  {facts: fact Name_Space.table,
   props: thm Net.net};
 
 fun make_facts facts props = Facts {facts = facts, props = props};
+
 val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
 
 
 (* named facts *)
 
 fun facts_of (Facts {facts, ...}) = facts;
 
 val space_of = #1 o facts_of;
 val table_of = #2 o facts_of;
+
+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;
 
 val defined = Symtab.defined o table_of;

 
 (* remove entries *)
 
 fun del name (Facts {facts = (space, tab), props}) =
   let
-    val space' = Name_Space.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
+    val space' = Name_Space.hide true name space handle ERROR _ => space;
     val tab' = Symtab.delete_safe name tab;
   in make_facts (space', tab') props end;
 
 fun hide fully name (Facts {facts = (space, tab), props}) =
   make_facts (Name_Space.hide fully name space, tab) props;