--- a/src/HOL/SMT/Examples/SMT_Examples.thy Mon Feb 08 17:12:38 2010 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Mon Feb 08 17:12:40 2010 +0100
@@ -17,7 +17,7 @@
the following option is set to "false":
*}
-declare [[smt_record=false]]
+declare [[smt_record=false]]