# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 11a442b472c72b746d467c77901cef1ef1d999ff
# Parent  11715564e2ade7e1cd4e21f70df0cf87e0734703
tune indentation

diff -r 11715564e2ad -r 11a442b472c7 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
@@ -1161,27 +1161,27 @@
           (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
         end
       and do_formula t accum =
-          case t of
-            (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
-            do_all t0 s1 T1 t1 accum
-          | @{const Trueprop} $ t1 =>
-            let val (m1, accum) = do_formula t1 accum in
-              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
-                     m1), accum)
-            end
-          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
-            consider_general_equals mdata true x t1 t2 accum
-          | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
-          | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
-            do_conjunction t0 t1 t2 accum
-          | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
-            do_all t0 s0 T1 t1 accum
-          | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
-            consider_general_equals mdata true x t1 t2 accum
-          | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
-          | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
-          | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
-                             \do_formula", [t])
+        case t of
+          (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+          do_all t0 s1 T1 t1 accum
+        | @{const Trueprop} $ t1 =>
+          let val (m1, accum) = do_formula t1 accum in
+            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
+             accum)
+          end
+        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
+          consider_general_equals mdata true x t1 t2 accum
+        | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+        | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
+          do_conjunction t0 t1 t2 accum
+        | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
+          do_all t0 s0 T1 t1 accum
+        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
+          consider_general_equals mdata true x t1 t2 accum
+        | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+        | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+        | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
+                           \do_formula", [t])
     in do_formula t end
 
 fun string_for_mtype_of_term ctxt asgs t M =