diff -r 57413334669d -r d9c247f7afa3 doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy	Tue Sep 21 10:02:50 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy	Tue Sep 21 14:36:13 2010 +0200
@@ -167,7 +167,7 @@
 *}
 
 
-subsection {* Datatype refinement involving invariants *}
+subsection {* Datatype refinement involving invariants \label{sec:invariant} *}
 
 text {*
   Datatype representation involving invariants require a dedicated