# HG changeset patch
# User blanchet
# Date 1335357201 -7200
# Node ID 0814fc93ab89c599c42b0ad8237bbd18c8733671
# Parent  f98bbb445c061a444eb71ad1d3bf39e20ba7999a
output SZS status as early as possible

diff -r f98bbb445c06 -r 0814fc93ab89 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 25 14:28:13 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 25 14:33:21 2012 +0200
@@ -667,6 +667,14 @@
             ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
              : problem_extension) =
       let
+        val _ =
+          print_t (fn () =>
+               "% SZS status " ^
+               (if genuine then
+                  if falsify then "CounterSatisfiable" else "Satisfiable"
+                else
+                  "Unknown") ^ "\n" ^
+               "% SZS output start FiniteModel")
         val (reconstructed_model, codatatypes_ok) =
           reconstruct_hol_model
               {show_datatypes = show_datatypes, show_skolems = show_skolems,
@@ -680,14 +688,7 @@
         fun assms_prop () =
           Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts)
       in
-        (print_t (fn () =>
-             "% SZS status " ^
-             (if genuine then
-                if falsify then "CounterSatisfiable" else "Satisfiable"
-              else
-                "Unknown") ^ "\n" ^
-             "% SZS output start FiniteModel");
-         pprint_a (Pretty.chunks
+        (pprint_a (Pretty.chunks
              [Pretty.blk (0,
                   (pstrs ((if mode = Auto_Try then "Auto " else "") ^
                           "Nitpick found a" ^