diff -r dc76ba24e81b -r c6b5d1e25cdd ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Jan 14 22:10:04 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Fri Feb 05 15:49:03 2010 +0100
@@ -2178,7 +2178,7 @@
 end"
 "Const (\"==\",\<dots>) $ 
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
-    (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
+    (Const (\"Algebras.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