src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41002 11a442b472c7
parent 41001 11715564e2ad
child 41003 7e2a7bd55a00
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -1161,27 +1161,27 @@
     1.4            (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
     1.5          end
     1.6        and do_formula t accum =
     1.7 -          case t of
     1.8 -            (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
     1.9 -            do_all t0 s1 T1 t1 accum
    1.10 -          | @{const Trueprop} $ t1 =>
    1.11 -            let val (m1, accum) = do_formula t1 accum in
    1.12 -              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
    1.13 -                     m1), accum)
    1.14 -            end
    1.15 -          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
    1.16 -            consider_general_equals mdata true x t1 t2 accum
    1.17 -          | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
    1.18 -          | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
    1.19 -            do_conjunction t0 t1 t2 accum
    1.20 -          | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
    1.21 -            do_all t0 s0 T1 t1 accum
    1.22 -          | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
    1.23 -            consider_general_equals mdata true x t1 t2 accum
    1.24 -          | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
    1.25 -          | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
    1.26 -          | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
    1.27 -                             \do_formula", [t])
    1.28 +        case t of
    1.29 +          (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
    1.30 +          do_all t0 s1 T1 t1 accum
    1.31 +        | @{const Trueprop} $ t1 =>
    1.32 +          let val (m1, accum) = do_formula t1 accum in
    1.33 +            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
    1.34 +             accum)
    1.35 +          end
    1.36 +        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
    1.37 +          consider_general_equals mdata true x t1 t2 accum
    1.38 +        | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
    1.39 +        | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
    1.40 +          do_conjunction t0 t1 t2 accum
    1.41 +        | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
    1.42 +          do_all t0 s0 T1 t1 accum
    1.43 +        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
    1.44 +          consider_general_equals mdata true x t1 t2 accum
    1.45 +        | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
    1.46 +        | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
    1.47 +        | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
    1.48 +                           \do_formula", [t])
    1.49      in do_formula t end
    1.50  
    1.51  fun string_for_mtype_of_term ctxt asgs t M =