diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -5,7 +5,7 @@
 
 header{*Implementation of a multiple-client allocator from a single-client allocator*}
 
-theory AllocImpl imports AllocBase Follows PPROD begin
+theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin
 
 
 (** State definitions.  OUTPUT variables are locals **)