src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Sun Jan 19 11:05:38 2014 +0100
+++ b/src/HOL/SMT.thy	Sun Jan 19 22:38:17 2014 +0100
@@ -204,9 +204,9 @@
 options.
 *}
 
-declare [[ cvc3_options = "", remote_cvc3_options = "" ]]
+declare [[ cvc3_options = "" ]]
 declare [[ yices_options = "" ]]
-declare [[ z3_options = "", remote_z3_options = "" ]]
+declare [[ z3_options = "" ]]
 
 text {*
 Enable the following option to use built-in support for datatypes and