diff -r a19a5179fbca -r 44fa9df44e6f IntEx.thy --- 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 \ ===> op \ ===> op \) ===> op \ ===> LIST_REL op \ ===> op \) foldl foldl" -apply (simp only: FUN_REL.simps) +apply (simp only: fun_rel.simps) apply (rule allI) apply (rule allI) apply (rule impI)