src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 34936 c4f04bee79f3
parent 34123 c4988215a691
child 34982 7b8c366e34a2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Jan 14 17:06:35 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Jan 20 10:38:06 2010 +0100
     1.3 @@ -121,8 +121,8 @@
     1.4  
     1.5  (* typ -> typ -> bool *)
     1.6  fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
     1.7 -    T = alpha_T orelse (not (is_fp_iterator_type T)
     1.8 -                        andalso exists (could_exist_alpha_subtype alpha_T) Ts)
     1.9 +    T = alpha_T orelse (not (is_fp_iterator_type T) andalso
    1.10 +                        exists (could_exist_alpha_subtype alpha_T) Ts)
    1.11    | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
    1.12  (* theory -> typ -> typ -> bool *)
    1.13  fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
    1.14 @@ -195,8 +195,8 @@
    1.15        let
    1.16          val C1 = do_type T1
    1.17          val C2 = do_type T2
    1.18 -        val a = if is_boolean_type (body_type T2)
    1.19 -                   andalso exists_alpha_sub_ctype_fresh C1 then
    1.20 +        val a = if is_boolean_type (body_type T2) andalso
    1.21 +                   exists_alpha_sub_ctype_fresh C1 then
    1.22                    V (Unsynchronized.inc max_fresh)
    1.23                  else
    1.24                    S Neg