# HG changeset patch
# User blanchet
# Date 1394794323 -3600
# Node ID 836b47c6531d0b0af8bbf3c917907adaf374790d
# Parent  1ef77430713b8dd328a8e2e05959e13e8195f8ed
tuning

diff -r 1ef77430713b -r 836b47c6531d src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:44:11 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:52:03 2014 +0100
@@ -59,10 +59,9 @@
   (case SMT2_Config.certificates_of ctxt of
     NONE =>
       if not (SMT2_Config.is_available ctxt name) then
-        error ("The SMT solver " ^ quote name ^ " is not installed.")
+        error ("The SMT solver " ^ quote name ^ " is not installed")
       else if Config.get ctxt SMT2_Config.debug_files = "" then
-        trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
-          (Cache_IO.run mk_cmd) input
+        trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run mk_cmd) input
       else
         let
           val base_path = Path.explode (Config.get ctxt SMT2_Config.debug_files)
diff -r 1ef77430713b -r 836b47c6531d src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Mar 14 11:44:11 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Mar 14 11:52:03 2014 +0100
@@ -112,7 +112,7 @@
     Z3_Non_Commercial_Accepted => f ()
   | Z3_Non_Commercial_Declined =>
       error (Pretty.string_of (Pretty.para
-        "The SMT solver Z3 may only be used for non-commercial applications."))
+        "The SMT solver Z3 may be used only for non-commercial applications."))
   | Z3_Non_Commercial_Unknown =>
       error (Pretty.string_of (Pretty.para
         ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \