# HG changeset patch
# User wenzelm
# Date 1256494465 -3600
# Node ID 351fc13613f2a815650324725b736844c00f55fc
# Parent  d11b89e7afd970c7b9db555b02faa1cab5531be2
export is_concealed;
tuned;

diff -r d11b89e7afd9 -r 351fc13613f2 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sun Oct 25 19:14:11 2009 +0100
+++ b/src/Pure/facts.ML	Sun Oct 25 19:14:25 2009 +0100
@@ -21,6 +21,7 @@
   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
@@ -44,7 +45,7 @@
 (** 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 *)
@@ -126,6 +127,7 @@
   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;
 
 
@@ -136,6 +138,8 @@
 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;
 
@@ -216,7 +220,7 @@
 
 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;