--- a/ProgTutorial/Essential.thy	Sun Dec 15 23:49:05 2013 +0000
+++ b/ProgTutorial/Essential.thy	Thu Mar 13 17:16:49 2014 +0000
@@ -609,9 +609,9 @@
   term constructor is defined (@{text "List"}) and also in which datatype
   (@{text "list"}). Even worse, some constants have a name involving
   type-classes. Consider for example the constants for @{term "zero"} and
-  \mbox{@{text "(op *)"}}:
-
-  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
+  \mbox{@{term "times"}}:
+
+  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" 
  "(Const (\"Groups.zero_class.zero\", \<dots>), 
  Const (\"Groups.times_class.times\", \<dots>))"}
 
@@ -2133,7 +2133,7 @@
 *}
 
 setup %gray{* 
-  Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) 
+  Term_Style.setup @{binding "my_strip_allq"} (Scan.succeed (K strip_allq)) 
 *}
 
 text {*
@@ -2185,7 +2185,7 @@
   val parser = Scan.repeat Args.name
   fun action xs = K (rename_allq xs #> strip_allq)
 in
-  Term_Style.setup "my_strip_allq2" (parser >> action)
+  Term_Style.setup @{binding "my_strip_allq2"} (parser >> action)
 end *}
 
 text {*