src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49029 f0ecfa9575a9
parent 49018 b2884253b421
child 49074 d8af889dcbe3
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 13:42:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 14:27:26 2012 +0200
     1.3 @@ -2039,7 +2039,7 @@
     1.4      val surj_unf_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_unf_thms;
     1.5      val unf_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_unf_thms;
     1.6      val unf_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_unf_thms;
     1.7 -    val unf_exhaust_thms = map (fn thm => thm RS @{thm exE}) unf_nchotomy_thms;
     1.8 +    val unf_exhaust_thms = map (fn thm => thm RS exE) unf_nchotomy_thms;
     1.9  
    1.10      val bij_fld_thms =
    1.11        map2 (fn thm1 => fn thm2 => @{thm o_bij} OF [thm1, thm2]) unf_o_fld_thms fld_o_unf_thms;
    1.12 @@ -2047,7 +2047,7 @@
    1.13      val surj_fld_thms = map (fn thm => thm RS @{thm bij_is_surj}) bij_fld_thms;
    1.14      val fld_nchotomy_thms = map (fn thm => thm RS @{thm surjD}) surj_fld_thms;
    1.15      val fld_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_fld_thms;
    1.16 -    val fld_exhaust_thms = map (fn thm => thm RS @{thm exE}) fld_nchotomy_thms;
    1.17 +    val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
    1.18  
    1.19      val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
    1.20        iffD1 OF [unf_inject, trans  OF [coiter, unf_fld RS sym]])