src/Tools/Code/code_namespace.ML
changeset 67521 6a27e86cc2e7
parent 59103 788db6d6b8a5
     1.1 --- a/src/Tools/Code/code_namespace.ML	Sun Jan 28 12:57:35 2018 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Jan 28 16:09:00 2018 +0100
     1.3 @@ -382,7 +382,7 @@
     1.4          val (name_fragments, _) = prep_sym sym;
     1.5          val (name_fragments', _) = prep_sym sym';
     1.6          val (name_fragments_common, (diff, diff')) =
     1.7 -          chop_prefix (op =) (name_fragments, name_fragments');
     1.8 +          chop_common_prefix (op =) (name_fragments, name_fragments');
     1.9          val is_cross_module = not (null diff andalso null diff');
    1.10          val dep = apply2 hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
    1.11          val add_edge = if is_cross_module andalso not cyclic_modules
    1.12 @@ -432,7 +432,7 @@
    1.13      fun deresolver prefix_fragments sym =
    1.14        let
    1.15          val (name_fragments, _) = prep_sym sym;
    1.16 -        val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
    1.17 +        val (_, (_, remainder)) = chop_common_prefix (op =) (prefix_fragments, name_fragments);
    1.18          val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment)
    1.19           of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
    1.20          val (base', _) = Code_Symbol.Graph.get_node nodes sym;