--- a/ProgTutorial/Essential.thy	Fri Dec 04 23:45:32 2009 +0100
+++ b/ProgTutorial/Essential.thy	Sun Dec 06 14:26:14 2009 +0100
@@ -683,7 +683,7 @@
   \end{exercise}
 *}
 
-section {* Unification and Matching *}
+section {* Unification and Matching\label{sec:univ} *}
 
 text {* 
   As seen earlier, Isabelle's terms and types may contain schematic term variables