src/HOL/Tools/SMT2/smt2_systems.ML
changeset 56131 836b47c6531d
parent 56125 e03c0f6ad1b6
child 56467 8d7d6f17c6a7
--- 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 \