--- a/ProgTutorial/FirstSteps.thy	Sun Jul 26 13:06:55 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Jul 26 18:13:50 2009 +0200
@@ -993,7 +993,7 @@
   type-classes. Consider for example the constants for @{term "zero"} and
   \mbox{@{text "(op *)"}}:
 
-  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" 
+  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
  "(Const (\"HOL.zero_class.zero\", \<dots>), 
  Const (\"HOL.times_class.times\", \<dots>))"}