--- a/src/HOL/ex/InductiveInvariant.thy	Tue Aug 02 10:03:14 2011 +0200
+++ b/src/HOL/ex/InductiveInvariant.thy	Tue Aug 02 10:36:50 2011 +0200
@@ -4,7 +4,7 @@
 
 header {* Some of the results in Inductive Invariants for Nested Recursion *}
 
-theory InductiveInvariant imports Main begin
+theory InductiveInvariant imports "~~/src/HOL/Library/Old_Recdef" begin
 
 text {* A formalization of some of the results in \emph{Inductive
   Invariants for Nested Recursion}, by Sava Krsti\'{c} and John