diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/While_Combinator_Example.thy
--- a/src/HOL/ex/While_Combinator_Example.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/While_Combinator_Example.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>An application of the While combinator\<close>
 
 theory While_Combinator_Example
-imports "~~/src/HOL/Library/While_Combinator"
+imports "HOL-Library.While_Combinator"
 begin
 
 text \<open>Computation of the @{term lfp} on finite sets via