src/Tools/Code/code_namespace.ML
changeset 43326 47cf4bc789aa
parent 40705 03f1266a066e
child 44338 700008399ee5
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -46,8 +46,7 @@
     1.4    let
     1.5      fun alias_fragments name = case module_alias name
     1.6       of SOME name' => Long_Name.explode name'
     1.7 -      | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
     1.8 -          (Long_Name.explode name);
     1.9 +      | NONE => map (fn name => fst (Name.variant name reserved)) (Long_Name.explode name);
    1.10      val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
    1.11    in
    1.12      fold (fn name => Symtab.update (name, Long_Name.explode module_prefix @ alias_fragments name))