# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 01f33bf79596a74cf21696031a476f1e293ef29e
# Parent  7e2a7bd55a00e3ddfa49aa6b5f5f6d8a7fc63ed0
tune parentheses and indentation

diff -r 7e2a7bd55a00 -r 01f33bf79596 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -1061,42 +1061,41 @@
             Plus => do_term t accum
           | Minus => consider_general_equals mdata false x t1 t2 accum
       in
-        (trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
-                             " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
-                             " : o\<^sup>" ^ string_for_sign sn ^ "?");
-         case t of
-           Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
-           do_quantifier x s1 T1 t1
-         | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
-         | @{const Trueprop} $ t1 =>
-           let val (m1, accum) = do_formula sn t1 accum in
-             (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
-                    m1), accum)
-           end
-         | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
-           do_quantifier x s1 T1 t1
-         | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
-           (case sn of
-              Plus => do_quantifier x0 s1 T1 t1'
-            | Minus =>
-              (* FIXME: Move elsewhere *)
-              do_term (@{const Not}
-                       $ (HOLogic.eq_const (domain_type T0) $ t1
-                          $ Abs (Name.uu, T1, @{const False}))) accum)
-         | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
-           do_equals x t1 t2
-         | Const (@{const_name Let}, _) $ t1 $ t2 =>
-           do_formula sn (betapply (t2, t1)) accum
-         | @{const Pure.conjunction} $ t1 $ t2 =>
-           do_connect meta_conj_triple false t1 t2 accum
-         | @{const "==>"} $ t1 $ t2 =>
-           do_connect meta_imp_triple true t1 t2 accum
-         | @{const Not} $ t1 =>
-           do_connect imp_triple true t1 @{const False} accum
-         | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
-         | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
-         | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
-         | _ => do_term t accum)
+        trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
+                            " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
+                            " : o\<^sup>" ^ string_for_sign sn ^ "?");
+        case t of
+          Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+          do_quantifier x s1 T1 t1
+        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
+        | @{const Trueprop} $ t1 =>
+          let val (m1, accum) = do_formula sn t1 accum in
+            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
+             accum)
+          end
+        | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
+          do_quantifier x s1 T1 t1
+        | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
+          (case sn of
+             Plus => do_quantifier x0 s1 T1 t1'
+           | Minus =>
+             (* FIXME: Move elsewhere *)
+             do_term (@{const Not}
+                      $ (HOLogic.eq_const (domain_type T0) $ t1
+                         $ Abs (Name.uu, T1, @{const False}))) accum)
+        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => do_equals x t1 t2
+        | Const (@{const_name Let}, _) $ t1 $ t2 =>
+          do_formula sn (betapply (t2, t1)) accum
+        | @{const Pure.conjunction} $ t1 $ t2 =>
+          do_connect meta_conj_triple false t1 t2 accum
+        | @{const "==>"} $ t1 $ t2 =>
+          do_connect meta_imp_triple true t1 t2 accum
+        | @{const Not} $ t1 =>
+          do_connect imp_triple true t1 @{const False} accum
+        | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
+        | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
+        | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
+        | _ => do_term t accum
       end
       |> tap (fn (m, (gamma, _)) =>
                  trace_msg (fn () => string_for_mcontext ctxt t gamma ^