--- a/ProgTutorial/Advanced.thy	Sun Feb 19 01:33:47 2012 +0000
+++ b/ProgTutorial/Advanced.thy	Tue Mar 20 09:39:44 2012 +0000
@@ -657,7 +657,7 @@
 
 local_setup %gray {* 
   Local_Theory.define ((@{binding "TrueConj"}, NoSyn), 
-      (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
+      ((@{binding "TrueConj_def"}, []), @{term "True \<and> True"})) #> snd *}
 
 text {* 
   Now querying the definition you obtain: