--- a/src/HOL/SMT/Examples/SMT_Examples.thy Wed Apr 07 17:24:44 2010 +0200
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Wed Apr 07 19:48:58 2010 +0200
@@ -17,7 +17,7 @@
the following option is set to "false":
*}
-declare [[smt_record=false]]
+declare [[smt_fixed=true]]