slightly tuned
authorhaftmann
Tue Oct 28 16:59:01 2008 +0100 (2008-10-28)
changeset 28705c77a9f5672f8
parent 28704 8703d17c5e68
child 28706 3fef773ae6b1
slightly tuned
src/Tools/code/code_ml.ML
     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