tuned
authorhaftmann
Mon Nov 22 09:19:34 2010 +0100 (2010-11-22)
changeset 406303b5c31e55540
parent 40629 f276d46d4ec0
child 40631 b3f85ba3dae4
child 40671 5e46057ba8e0
tuned
src/Tools/Code/code_namespace.ML
     1.1 --- a/src/Tools/Code/code_namespace.ML	Mon Nov 22 09:18:25 2010 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Mon Nov 22 09:19:34 2010 +0100
     1.3 @@ -118,9 +118,9 @@
     1.4              Long_Name.append (the (AList.lookup (op =) import_tab name))
     1.5                (base_deresolver name))) imported_names
     1.6        end;
     1.7 -    val name_tabs = AList.make (uncurry classify_names o Graph.get_node flat_program)
     1.8 -      (Graph.keys flat_program);
     1.9 -    val deresolver_tab = fold Symtab.update name_tabs Symtab.empty;
    1.10 +    val deresolver_tab = Symtab.make (AList.make
    1.11 +      (uncurry classify_names o Graph.get_node flat_program)
    1.12 +        (Graph.keys flat_program));
    1.13      fun deresolver module_name name =
    1.14        the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
    1.15        handle Option => error ("Unknown statement name: " ^ labelled_name name);