src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 33732 385381514eed
parent 33580 45c33e97cb86
child 33852 3a586209151e
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Nov 16 10:24:28 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Nov 16 11:03:08 2009 +0100
     1.3 @@ -784,8 +784,8 @@
     1.4    let
     1.5      (* typ -> ctype *)
     1.6      val ctype_for = fresh_ctype_for_type cdata
     1.7 -    (* term -> accumulator -> accumulator *)
     1.8 -    val do_term = snd oo consider_term cdata
     1.9 +    (* term -> accumulator -> ctype * accumulator *)
    1.10 +    val do_term = consider_term cdata
    1.11      (* sign -> term -> accumulator -> accumulator *)
    1.12      fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
    1.13        | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
    1.14 @@ -810,8 +810,11 @@
    1.15            (* term -> term -> accumulator *)
    1.16            fun do_equals t1 t2 =
    1.17              case sn of
    1.18 -              Pos => do_term t accum
    1.19 -            | Neg => fold do_term [t1, t2] accum
    1.20 +              Pos => do_term t accum |> snd
    1.21 +            | Neg => let
    1.22 +                       val (C1, accum) = do_term t1 accum
    1.23 +                       val (C2, accum) = do_term t2 accum
    1.24 +                     in accum ||> add_ctypes_equal C1 C2 end
    1.25          in
    1.26            case t of
    1.27              Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
    1.28 @@ -839,10 +842,10 @@
    1.29            | @{const "op -->"} $ t1 $ t2 =>
    1.30              accum |> do_contra_formula t1 |> do_co_formula t2
    1.31            | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
    1.32 -            accum |> do_term t1 |> fold do_co_formula [t2, t3]
    1.33 +            accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3]
    1.34            | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.35              do_co_formula (betapply (t2, t1)) accum
    1.36 -          | _ => do_term t accum
    1.37 +          | _ => do_term t accum |> snd
    1.38          end
    1.39          |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
    1.40                                   Syntax.string_of_term ctxt t ^
    1.41 @@ -873,7 +876,7 @@
    1.42      I
    1.43    else
    1.44      let
    1.45 -      (* term -> accumulator -> accumulator *)
    1.46 +      (* term -> accumulator -> ctype * accumulator *)
    1.47        val do_term = consider_term cdata
    1.48        (* typ -> term -> accumulator -> accumulator *)
    1.49        fun do_all abs_T body_t accum =