src/HOL/Product_Type.thy
changeset 45607 16b4f5774621
parent 45205 2825ce94fd4d
child 45662 4f7c05990420
--- a/src/HOL/Product_Type.thy	Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Product_Type.thy	Sun Nov 20 21:07:10 2011 +0100
@@ -625,7 +625,7 @@
   Setup of internal @{text split_rule}.
 *}
 
-lemmas prod_caseI = prod.cases [THEN iffD2, standard]
+lemmas prod_caseI = prod.cases [THEN iffD2]
 
 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
   by (fact splitI2)