src/HOL/Tools/SMT2/smt2_systems.ML

 fun if_z3_non_commercial f =
   (case z3_non_commercial () of
     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 \
          \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
          \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))