--- a/IntEx.thy	Wed Oct 28 17:38:37 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 18:08:38 2009 +0100
@@ -111,7 +111,7 @@
   done
 
 lemma ho_plus_rsp:
-  "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
+  "(intrel ===> intrel ===> intrel) my_plus my_plus"
   by (simp)
 
 ML {* val consts = [@{const_name "my_plus"}] *}