# HG changeset patch # User haftmann # Date 1290413974 -3600 # Node ID 3b5c31e55540321336e0f575261a9fc56fb709a7 # Parent f276d46d4ec01958ec86507bf048552bd98c84af tuned diff -r f276d46d4ec0 -r 3b5c31e55540 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Mon Nov 22 09:18:25 2010 +0100 +++ b/src/Tools/Code/code_namespace.ML Mon Nov 22 09:19:34 2010 +0100 @@ -118,9 +118,9 @@ Long_Name.append (the (AList.lookup (op =) import_tab name)) (base_deresolver name))) imported_names end; - val name_tabs = AList.make (uncurry classify_names o Graph.get_node flat_program) - (Graph.keys flat_program); - val deresolver_tab = fold Symtab.update name_tabs Symtab.empty; + val deresolver_tab = Symtab.make (AList.make + (uncurry classify_names o Graph.get_node flat_program) + (Graph.keys flat_program)); fun deresolver module_name name = the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name) handle Option => error ("Unknown statement name: " ^ labelled_name name);