diff -r dc76ba24e81b -r c6b5d1e25cdd ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Thu Jan 14 22:10:04 2010 +0100
+++ b/ProgTutorial/Essential.thy	Fri Feb 05 15:49:03 2010 +0100
@@ -39,7 +39,7 @@
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
 "Const (\"op =\", \<dots>) $ 
-  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+  (Const (\"Algebras.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
   the internal representation corresponding to the datatype @{ML_type_ind "term"}, 
@@ -533,8 +533,8 @@
   \mbox{@{text "(op *)"}}:
 
   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
- "(Const (\"HOL.zero_class.zero\", \<dots>), 
- Const (\"HOL.times_class.times\", \<dots>))"}
+ "(Const (\"Algebras.zero_class.zero\", \<dots>), 
+ Const (\"Algebras.times_class.times\", \<dots>))"}
 
   While you could use the complete name, for example 
   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or