| changeset 60282 | 496fa0fc91b1 |
| parent 59990 | a81dc82ecba3 |
| child 60284 | 014b86186c49 |
--- 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 *)