src/Tools/Code/code_namespace.ML
changeset 40705 03f1266a066e
parent 40630 3b5c31e55540
child 43326 47cf4bc789aa
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Nov 25 00:32:30 2010 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Nov 25 15:40:15 2010 +0100
     1.3 @@ -121,9 +121,11 @@
     1.4      val deresolver_tab = Symtab.make (AList.make
     1.5        (uncurry classify_names o Graph.get_node flat_program)
     1.6          (Graph.keys flat_program));
     1.7 -    fun deresolver module_name name =
     1.8 -      the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
     1.9 -      handle Option => error ("Unknown statement name: " ^ labelled_name name);
    1.10 +    fun deresolver "" name =
    1.11 +          Long_Name.append (fst (dest_name name)) (base_deresolver name)
    1.12 +      | deresolver module_name name =
    1.13 +          the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
    1.14 +          handle Option => error ("Unknown statement name: " ^ labelled_name name);
    1.15  
    1.16    in { deresolver = deresolver, flat_program = flat_program } end;
    1.17