1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Oct 29 16:06:28 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Oct 29 21:57:59 2009 +0100
     1.3 @@ -708,7 +708,7 @@
     1.4                    (CFun (left_set_C, S Neg,
     1.5                           CFun (right_set_C, S Neg, left_set_C)),
     1.6                     (gamma, cset |> add_ctype_is_right_unique right_set_C
     1.7 -                          (* FIXME: |> add_is_sub_ctype right_set_C left_set_C *)))
     1.8 +                                |> add_is_sub_ctype right_set_C left_set_C))
     1.9                  end
    1.10                | @{const_name ord_fun_inst.less_eq_fun} =>
    1.11                  do_fragile_set_operation T accum
    1.12 @@ -784,10 +784,8 @@
    1.13    let
    1.14      (* typ -> ctype *)
    1.15      val ctype_for = fresh_ctype_for_type cdata
    1.16 -    (* term -> accumulator -> ctype * accumulator *)
    1.17 -    val do_term = consider_term cdata
    1.18      (* term -> accumulator -> accumulator *)
    1.19 -    val do_boolean_term = snd oo do_term
    1.20 +    val do_term = snd oo consider_term cdata
    1.21      (* sign -> term -> accumulator -> accumulator *)
    1.22      fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
    1.23        | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
    1.24 @@ -812,11 +810,8 @@
    1.25            (* term -> term -> accumulator *)
    1.26            fun do_equals t1 t2 =
    1.27              case sn of
    1.28 -              Pos => do_boolean_term t accum
    1.29 -            | Neg => let
    1.30 -                       val (C1, accum) = do_term t1 accum
    1.31 -                       val (C2, accum) = do_term t2 accum
    1.32 -                     in accum (* FIXME: ||> add_ctypes_equal C1 C2 *) end
    1.33 +              Pos => do_term t accum
    1.34 +            | Neg => fold do_term [t1, t2] accum
    1.35          in
    1.36            case t of
    1.37              Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
    1.38 @@ -844,10 +839,10 @@
    1.39            | @{const "op -->"} $ t1 $ t2 =>
    1.40              accum |> do_contra_formula t1 |> do_co_formula t2
    1.41            | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
    1.42 -            accum |> do_boolean_term t1 |> do_co_formula t2 |> do_co_formula t3
    1.43 +            accum |> do_term t1 |> fold do_co_formula [t2, t3]
    1.44            | Const (@{const_name Let}, _) $ t1 $ t2 =>
    1.45              do_co_formula (betapply (t2, t1)) accum
    1.46 -          | _ => do_boolean_term t accum
    1.47 +          | _ => do_term t accum
    1.48          end
    1.49          |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
    1.50                                   Syntax.string_of_term ctxt t ^