--- a/src/HOL/SMT/SMT.thy Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/SMT.thy Wed Apr 07 20:40:42 2010 +0200
@@ -76,8 +76,4 @@
declare [[ smt_trace = false ]]
-text {* Unfold (some) definitions passed to the SMT solver: *}
-
-declare [[ smt_unfold_defs = true ]]
-
end