# HG changeset patch
# User wenzelm
# Date 1431530832 -7200
# Node ID 496fa0fc91b1734f9b2c3fd6c70b1c7e35f6e713
# Parent  6b01377b95b9d8d9e015a31ccbb54bd9e7fcf273
more permissive operation: allow to print undeclared name space entries, e.g. print_simpset with "record" simproc;

diff -r 6b01377b95b9 -r 496fa0fc91b1 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat May 09 20:40:28 2015 +0200
+++ b/src/Pure/General/name_space.ML	Wed May 13 17:27:12 2015 +0200
@@ -179,7 +179,8 @@
 
 fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
 
-fun is_concealed space name = #concealed (the_entry space name);
+fun is_concealed space name =
+  #concealed (the_entry space name) handle ERROR _ => false;
 
 
 (* intern *)