tuned
authorhaftmann
Wed Dec 02 11:29:49 2009 +0100 (2009-12-02 ago)
changeset 3397074db95c74f89
parent 33969 1e7ca47c6c3d
child 33971 9c7fa7f76950
tuned
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Nov 30 12:28:12 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Dec 02 11:29:49 2009 +0100
     1.3 @@ -370,19 +370,18 @@
     1.4  
     1.5  fun find_nonempty descr is i =
     1.6    let
     1.7 -    val (_, _, constrs) = the (AList.lookup (op =) descr i);
     1.8      fun arg_nonempty (_, DtRec i) = if member (op =) is i
     1.9            then NONE
    1.10            else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
    1.11        | arg_nonempty _ = SOME 0;
    1.12 -    fun max xs = Library.foldl
    1.13 -      (fn (NONE, _) => NONE
    1.14 -        | (SOME i, SOME j) => SOME (Int.max (i, j))
    1.15 -        | (_, NONE) => NONE) (SOME 0, xs);
    1.16 +    fun max_inf (SOME i) (SOME j) = Integer.max i j
    1.17 +      | max_inf _ _ = NONE;
    1.18 +    fun max xs = fold max_inf xs (SOME 0);
    1.19 +    val (_, _, constrs) = the (AList.lookup (op =) descr i);
    1.20      val xs = sort (int_ord o pairself snd)
    1.21        (map_filter (fn (s, dts) => Option.map (pair s)
    1.22          (max (map (arg_nonempty o strip_dtyp) dts))) constrs)
    1.23 -  in case xs of [] => NONE | x :: _ => SOME x end;
    1.24 +  in if null xs then NONE else SOME (hd xs) end;
    1.25  
    1.26  fun find_shortest_path descr i = find_nonempty descr [i] i;
    1.27