--- a/Quot/Examples/IntEx2.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -108,7 +108,7 @@
 
 lemma mult_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
-apply(simp only: fun_rel.simps)
+apply(simp only: fun_rel_def)
 apply(rule allI | rule impI)+
 apply(rule equivp_transp[OF int_equivp])
 apply(rule mult_raw_fst)