diff -r c5d0f19ef7cb -r 0f8c8ac6cc0e doc-src/ZF/FOL_examples.thy
--- a/doc-src/ZF/FOL_examples.thy	Thu Jul 26 14:29:54 2012 +0200
+++ b/doc-src/ZF/FOL_examples.thy	Thu Jul 26 14:44:07 2012 +0200
@@ -1,6 +1,6 @@
 header{*Examples of Classical Reasoning*}
 
-theory FOL_examples imports FOL begin
+theory FOL_examples imports "~~/src/FOL/FOL" begin
 
 lemma "EX y. ALL x. P(y)-->P(x)"
   --{* @{subgoals[display,indent=0,margin=65]} *}