diff -r de58f4d939e1 -r 609c072edf90 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Sep 15 12:27:13 2003 +0200
+++ b/src/HOL/Product_Type.thy	Mon Sep 15 14:00:43 2003 +0200
@@ -276,10 +276,10 @@
 lemma curryI [intro!]: "f (a,b) ==> curry f a b"
   by (simp add: curry_def)
 
-lemma curryD [dest]: "curry f a b ==> f (a,b)"
+lemma curryD [dest!]: "curry f a b ==> f (a,b)"
   by (simp add: curry_def)
 
-lemma curryE [elim!]: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
+lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q"
   by (simp add: curry_def)
 
 lemma curry_conv [simp]: "curry f a b = f (a,b)"