# HG changeset patch
# User blanchet
# Date 1256849879 -3600
# Node ID 113e235e84e3f4b35cfd3bd277f74fb9197a167b
# Parent  e61ad1690c11653de330d25162e3ec2eb59e724a
eliminate two FIXMEs in Nitpick's monotonicity check code

diff -r e61ad1690c11 -r 113e235e84e3 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Oct 29 16:06:28 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Oct 29 21:57:59 2009 +0100
@@ -708,7 +708,7 @@
                   (CFun (left_set_C, S Neg,
                          CFun (right_set_C, S Neg, left_set_C)),
                    (gamma, cset |> add_ctype_is_right_unique right_set_C
-                          (* FIXME: |> add_is_sub_ctype right_set_C left_set_C *)))
+                                |> add_is_sub_ctype right_set_C left_set_C))
                 end
               | @{const_name ord_fun_inst.less_eq_fun} =>
                 do_fragile_set_operation T accum
@@ -784,10 +784,8 @@
   let
     (* typ -> ctype *)
     val ctype_for = fresh_ctype_for_type cdata
-    (* term -> accumulator -> ctype * accumulator *)
-    val do_term = consider_term cdata
     (* term -> accumulator -> accumulator *)
-    val do_boolean_term = snd oo do_term
+    val do_term = snd oo consider_term cdata
     (* sign -> term -> accumulator -> accumulator *)
     fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
       | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
@@ -812,11 +810,8 @@
           (* term -> term -> accumulator *)
           fun do_equals t1 t2 =
             case sn of
-              Pos => do_boolean_term t accum
-            | Neg => let
-                       val (C1, accum) = do_term t1 accum
-                       val (C2, accum) = do_term t2 accum
-                     in accum (* FIXME: ||> add_ctypes_equal C1 C2 *) end
+              Pos => do_term t accum
+            | Neg => fold do_term [t1, t2] accum
         in
           case t of
             Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
@@ -844,10 +839,10 @@
           | @{const "op -->"} $ t1 $ t2 =>
             accum |> do_contra_formula t1 |> do_co_formula t2
           | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
-            accum |> do_boolean_term t1 |> do_co_formula t2 |> do_co_formula t3
+            accum |> do_term t1 |> fold do_co_formula [t2, t3]
           | Const (@{const_name Let}, _) $ t1 $ t2 =>
             do_co_formula (betapply (t2, t1)) accum
-          | _ => do_boolean_term t accum
+          | _ => do_term t accum
         end
         |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
                                  Syntax.string_of_term ctxt t ^