src/HOL/ex/While_Combinator_Example.thy

--- a/src/HOL/ex/While_Combinator_Example.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/While_Combinator_Example.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* An application of the While combinator *}
 
 theory While_Combinator_Example
-imports While_Combinator
+imports "~~/src/HOL/Library/While_Combinator"
 begin
 
 text {* Computation of the @{term lfp} on finite sets via