# HG changeset patch
# User wenzelm
# Date 1205615251 -3600
# Node ID e025bf1cc0f1649980fc2e5f18c2c88bcf70b3c0
# Parent  9d2c375e242b5a0541bcffc317bdf63ca816b3f3
del: hide in name space;

diff -r 9d2c375e242b -r e025bf1cc0f1 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sat Mar 15 22:07:29 2008 +0100
+++ b/src/Pure/facts.ML	Sat Mar 15 22:07:31 2008 +0100
@@ -77,6 +77,9 @@
   in make_facts facts' props' end;
 
 fun del name (Facts {facts = (space, tab), props}) =
-  make_facts (space, Symtab.delete_safe name tab) props;
+  let
+    val space' = NameSpace.hide true name space handle ERROR _ => space;
+    val tab' = Symtab.delete_safe name tab;
+  in make_facts (space', tab') props end;
 
 end;