--- a/IntEx.thy	Wed Nov 04 10:31:20 2009 +0100
+++ b/IntEx.thy	Wed Nov 04 10:43:33 2009 +0100
@@ -39,7 +39,7 @@
 quotient_def 
   PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
-  "PLUS x y \<equiv> my_plus x y"
+  "PLUS \<equiv> my_plus"
 
 term PLUS
 thm PLUS_def