src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 41046 f2e94005d283
parent 41045 2a41709f34c1
child 41047 9f1d3fcef1ca
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -424,6 +424,7 @@
     1.4     (@{const_name converse}, 1),
     1.5     (@{const_name trancl}, 1),
     1.6     (@{const_name rel_comp}, 2),
     1.7 +   (@{const_name prod}, 2),
     1.8     (@{const_name image}, 2),
     1.9     (@{const_name finite}, 1),
    1.10     (@{const_name unknown}, 0),
    1.11 @@ -1645,9 +1646,14 @@
    1.12                  s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
    1.13        | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
    1.14          do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
    1.15 -      | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
    1.16 -        s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
    1.17 -                        map (do_term depth Ts) [t1, t2])
    1.18 +      | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
    1.19 +        $ t1 $ (t2 as Abs (_, _, t2')) =>
    1.20 +        if loose_bvar1 (t2', 0) then
    1.21 +          s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2])
    1.22 +        else
    1.23 +          do_term depth Ts
    1.24 +                  (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
    1.25 +                   $ t1 $ incr_boundvars ~1 t2')
    1.26        | Const (x as (@{const_name distinct},
    1.27                 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
    1.28          $ (t1 as _ $ _) =>