--- a/src/Pure/General/name_space.ML Tue Mar 31 20:18:10 2015 +0200
+++ b/src/Pure/General/name_space.ML Tue Mar 31 21:12:22 2015 +0200
@@ -166,18 +166,17 @@
(* intern *)
fun intern' (Name_Space {internals, ...}) xname =
- (case Change_Table.lookup internals xname of
- NONE => (xname, true)
- | SOME ([], []) => (xname, true)
- | SOME ([name], _) => (name, true)
- | SOME (name :: _, _) => (name, false)
- | SOME ([], name' :: _) => (Long_Name.hidden name', true));
+ (case the_default ([], []) (Change_Table.lookup internals xname) of
+ ([name], _) => (name, true)
+ | (name :: _, _) => (name, false)
+ | ([], []) => (Long_Name.hidden xname, true)
+ | ([], name' :: _) => (Long_Name.hidden name', true));
val intern = #1 oo intern';
fun get_accesses (Name_Space {entries, ...}) name =
(case Change_Table.lookup entries name of
- NONE => [name]
+ NONE => []
| SOME (externals, _) => externals);
fun valid_accesses (Name_Space {internals, ...}) name =