diff -r daab96c3e2a9 -r d60f6b41bf2d src/HOL/ex/FinFunPred.thy
--- a/src/HOL/ex/FinFunPred.thy	Wed May 30 10:04:05 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 16:05:06 2012 +0200
@@ -4,7 +4,7 @@
   Predicates modelled as FinFuns
 *}
 
-theory FinFunPred imports "~~/src/HOL/Library/FinFun" begin
+theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin
 
 text {* Instantiate FinFun predicates just like predicates *}