diff -r da5fcc0f6c52 -r 65cdd08bd7fd doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Aug 08 13:40:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Aug 08 13:48:38 2011 +0200
@@ -1,5 +1,5 @@
 theory HOL_Specific
-imports Base Main
+imports Base Main "~~/src/HOL/Library/Old_Recdef"
 begin
 
 chapter {* Isabelle/HOL \label{ch:hol} *}