--- a/IntEx.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -243,7 +243,7 @@
 (* I believe it's true. *)
 lemma foldl_rsp[quotient_rsp]:
   "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
-apply (simp only: FUN_REL.simps)
+apply (simp only: fun_rel.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)