clarified signature;

--- a/src/Pure/library.ML	Sun Jan 28 12:57:35 2018 +0100
+++ b/src/Pure/library.ML	Sun Jan 28 16:09:00 2018 +0100
@@ -101,8 +101,8 @@
   val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
-  val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   val prefixes1: 'a list -> 'a list list
   val prefixes: 'a list -> 'a list list
   val suffixes1: 'a list -> 'a list list
@@ -540,14 +540,6 @@
             if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
   in  take([], xs)  end;
 
-fun chop_prefix eq ([], ys) = ([], ([], ys))
-  | chop_prefix eq (xs, []) = ([], (xs, []))
-  | chop_prefix eq (xs as x :: xs', ys as y :: ys') =
-      if eq (x, y) then
-        let val (ps', xys'') = chop_prefix eq (xs', ys')
-        in (x :: ps', xys'') end
-      else ([], (xs, ys));
-
 (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
    where xi is the last element that does not satisfy the predicate*)
 fun take_suffix _ [] = ([], [])
@@ -556,6 +548,14 @@
         ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
       | (prfx, sffx) => (x :: prfx, sffx));
 
+fun chop_common_prefix eq ([], ys) = ([], ([], ys))
+  | chop_common_prefix eq (xs, []) = ([], (xs, []))
+  | chop_common_prefix eq (xs as x :: xs', ys as y :: ys') =
+      if eq (x, y) then
+        let val (ps', xys'') = chop_common_prefix eq (xs', ys')
+        in (x :: ps', xys'') end
+      else ([], (xs, ys));
+
 fun prefixes1 [] = []
   | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
 

--- a/src/Tools/Code/code_namespace.ML	Sun Jan 28 12:57:35 2018 +0100
+++ b/src/Tools/Code/code_namespace.ML	Sun Jan 28 16:09:00 2018 +0100
@@ -382,7 +382,7 @@
         val (name_fragments, _) = prep_sym sym;
         val (name_fragments', _) = prep_sym sym';
         val (name_fragments_common, (diff, diff')) =
-          chop_prefix (op =) (name_fragments, name_fragments');
+          chop_common_prefix (op =) (name_fragments, name_fragments');
         val is_cross_module = not (null diff andalso null diff');
         val dep = apply2 hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
         val add_edge = if is_cross_module andalso not cyclic_modules
@@ -432,7 +432,7 @@
     fun deresolver prefix_fragments sym =
       let
         val (name_fragments, _) = prep_sym sym;
-        val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
+        val (_, (_, remainder)) = chop_common_prefix (op =) (prefix_fragments, name_fragments);
         val nodes = fold (fn name_fragment => fn nodes => case Code_Symbol.Graph.get_node nodes (Code_Symbol.Module name_fragment)
          of (_, Module (_, nodes)) => nodes) name_fragments hierarchical_program;
         val (base', _) = Code_Symbol.Graph.get_node nodes sym;