diff -r f399b6855546 -r aee4abd02db1 ProgTutorial/Appendix.thy
--- a/ProgTutorial/Appendix.thy	Wed Dec 02 02:34:09 2009 +0100
+++ b/ProgTutorial/Appendix.thy	Wed Dec 02 03:46:32 2009 +0100
@@ -25,10 +25,7 @@
   
   \item user space type systems (in the form that already exists)
 
-  \item unification and typing algorithms 
-  (@{ML_file "Pure/pattern.ML"} implements HOPU)
-
-  \item useful datastructures: discrimination nets, association lists
+  \item useful datastructures: discrimination nets, graphs, association lists
 
   \item Brief history of Isabelle
   \end{itemize}