diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Appendix.thy
--- a/CookBook/Appendix.thy	Tue Mar 17 17:32:12 2009 +0100
+++ b/CookBook/Appendix.thy	Wed Mar 18 03:03:51 2009 +0100
@@ -10,7 +10,7 @@
 chapter {* Recipes *}
 
 text {*
-  Possible further topics: 
+  Possible topics: 
 
   \begin{itemize}
   \item translations/print translations; 
@@ -18,7 +18,8 @@
   
   \item user space type systems (in the form that already exists)
 
-  \item unification and typing algorithms
+  \item unification and typing algorithms 
+  (@{ML_file "Pure/pattern.ML"} implements HOPU)
 
   \item useful datastructures: discrimination nets, association lists
   \end{itemize}