# HG changeset patch
# User wenzelm
# Date 1433006961 -7200
# Node ID ee6f9a97205dbd4c58775aa68c689acfd0433241
# Parent  599c4a27785c9ea68871e3e3e286c6fa193b220b
tuned message;

diff -r 599c4a27785c -r ee6f9a97205d src/HOL/Library/Old_SMT/old_smt_config.ML
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Sat May 30 19:28:51 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_config.ML	Sat May 30 19:29:21 2015 +0200
@@ -86,7 +86,7 @@
     |> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options"))
         (Scan.lift (@{keyword "="} |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
-        ("Additional command line options for SMT solver " ^ quote name))
+        ("additional command line options for SMT solver " ^ quote name))
 
 fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
 
diff -r 599c4a27785c -r ee6f9a97205d src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Sat May 30 19:28:51 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Sat May 30 19:29:21 2015 +0200
@@ -105,7 +105,7 @@
     |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
         (Scan.lift (@{keyword "="} |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
-        ("Additional command line options for SMT solver " ^ quote name))
+        ("additional command line options for SMT solver " ^ quote name))
 
 fun all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt)))