src/Tools/Code/code_namespace.ML
changeset 51930 52fd62618631
parent 47576 b32aae03e3d6
child 52138 e21426f244aa
equal deleted inserted replaced
51929:5e8a0b8bb070 51930:52fd62618631
   123         (Graph.keys flat_program));
   123         (Graph.keys flat_program));
   124     fun deresolver "" name =
   124     fun deresolver "" name =
   125           Long_Name.append (fst (dest_name name)) (base_deresolver name)
   125           Long_Name.append (fst (dest_name name)) (base_deresolver name)
   126       | deresolver module_name name =
   126       | deresolver module_name name =
   127           the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
   127           the (Symtab.lookup (the (Symtab.lookup deresolver_tab module_name)) name)
   128           handle Option => error ("Unknown statement name: " ^ labelled_name name);
   128           handle Option.Option => error ("Unknown statement name: " ^ labelled_name name);
   129 
   129 
   130   in { deresolver = deresolver, flat_program = flat_program } end;
   130   in { deresolver = deresolver, flat_program = flat_program } end;
   131 
   131 
   132 
   132 
   133 (** hierarchical program structure **)
   133 (** hierarchical program structure **)