diff -r 487427a02bee -r f0ecfa9575a9 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 13:42:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 14:27:26 2012 +0200
@@ -2039,7 +2039,7 @@
     val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms;
     val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms;
     val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms;
-    val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms;
+    val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms;
 
     val bij_fld_thms =
       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms;
@@ -2047,7 +2047,7 @@
     val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms;
     val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms;
     val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
-    val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms;
+    val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
 
     val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
       iffD1 OF [unf_inject, trans  OF [coiter, unf_fld RS sym]])