diff -r eaf0ffea11aa -r 446cfc760ccf src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/SMT.thy	Tue Mar 27 16:59:13 2012 +0300
@@ -272,16 +272,16 @@
 declare [[ smt_certificates = "" ]]
 
 text {*
-The option @{text smt_fixed} controls whether only stored
-certificates are should be used or invocation of an SMT solver is
-allowed.  When set to @{text true}, no SMT solver will ever be
+The option @{text smt_read_only_certificates} controls whether only
+stored certificates are should be used or invocation of an SMT solver
+is allowed.  When set to @{text true}, no SMT solver will ever be
 invoked and only the existing certificates found in the configured
 cache are used;  when set to @{text false} and there is no cached
 certificate for some proposition, then the configured SMT solver is
 invoked.
 *}
 
-declare [[ smt_fixed = false ]]
+declare [[ smt_read_only_certificates = false ]]