--- a/ProgTutorial/Tactical.thy	Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Sun Mar 07 21:15:05 2010 +0100
@@ -2178,7 +2178,7 @@
 end"
 "Const (\"==\",\<dots>) $ 
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
-    (Const (\"Algebras.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
+    (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
 
   The argument @{ML true} in @{ML beta_conversion in Thm} indicates that 
   the right-hand side should be fully beta-normalised. If instead