diff -r e7ecbe86d22e -r 93a7365fb4ee doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Fri Sep 03 22:57:21 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Fri Sep 03 23:54:48 2010 +0200
@@ -1,6 +1,6 @@
 theory Examples imports Main Binomial begin
 
-ML "eta_contract := false"
+declare [[eta_contract = false]]
 ML "Pretty.margin_default := 64"
 
 text{*membership, intersection *}