src/Tools/code/code_ml.ML
changeset 28705 c77a9f5672f8
parent 28673 d746a8c12c43
child 28708 a1a436f09ec6
     1.1 --- a/src/Tools/code/code_ml.ML	Tue Oct 28 16:59:00 2008 +0100
     1.2 +++ b/src/Tools/code/code_ml.ML	Tue Oct 28 16:59:01 2008 +0100
     1.3 @@ -800,7 +800,7 @@
     1.4            in if module_name = module_name' then
     1.5              map_node module_name_path (Graph.add_edge (name, name'))
     1.6            else let
     1.7 -            val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
     1.8 +            val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
     1.9                (module_name_path, NameSpace.explode module_name');
    1.10            in
    1.11              map_node common