src/HOL/Codatatype/Tools/bnf_gfp.ML

       map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) fld_o_unf_thms unf_o_fld_thms;
     val inj_unf_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_unf_thms;
     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;
     val inj_fld_thms = map (fn thm => thm RS @{thm bij_is_inj}) bij_fld_thms;
     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]])
       unf_inject_thms coiter_thms unf_fld_thms;