# HG changeset patch
# User blanchet
# Date 1288083568 -7200
# Node ID f2a14b6effcf8961b0c5479206c0a891e3db3d3e
# Parent  04a05b2a7a369b6bc86f140835b53d4f5547052a
whitespace tuning

diff -r 04a05b2a7a36 -r f2a14b6effcf src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 26 10:57:04 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 26 10:59:28 2010 +0200
@@ -505,29 +505,29 @@
   end
 
 fun solve max_var (lits, comps, sexps) =
-    let
-      fun do_assigns assigns =
-        SOME (literals_from_assignments max_var assigns lits
-              |> tap print_solution)
-      val _ = print_problem lits comps sexps
-      val prop = PropLogic.all (map prop_for_literal lits @
-                                map prop_for_comp comps @
-                                map prop_for_sign_expr sexps)
-      val default_val = bool_from_sign Minus
-    in
-      if PropLogic.eval (K default_val) prop then
-        do_assigns (K (SOME default_val))
-      else
-        let
-          (* use the first ML solver (to avoid startup overhead) *)
-          val solvers = !SatSolver.solvers
-                        |> filter (member (op =) ["dptsat", "dpll"] o fst)
-        in
-          case snd (hd solvers) prop of
-            SatSolver.SATISFIABLE assigns => do_assigns assigns
-          | _ => NONE
-        end
-    end
+  let
+    fun do_assigns assigns =
+      SOME (literals_from_assignments max_var assigns lits
+            |> tap print_solution)
+    val _ = print_problem lits comps sexps
+    val prop = PropLogic.all (map prop_for_literal lits @
+                              map prop_for_comp comps @
+                              map prop_for_sign_expr sexps)
+    val default_val = bool_from_sign Minus
+  in
+    if PropLogic.eval (K default_val) prop then
+      do_assigns (K (SOME default_val))
+    else
+      let
+        (* use the first ML solver (to avoid startup overhead) *)
+        val solvers = !SatSolver.solvers
+                      |> filter (member (op =) ["dptsat", "dpll"] o fst)
+      in
+        case snd (hd solvers) prop of
+          SatSolver.SATISFIABLE assigns => do_assigns assigns
+        | _ => NONE
+      end
+  end
 
 type mtype_schema = mtyp * constraint_set
 type mtype_context =