changeset 52659 | 58b87aa4dc3b |
parent 52635 | 4f84b730c489 |
child 52731 | dacd47a0633f |
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Jul 15 14:23:51 2013 +0200 @@ -2219,7 +2219,7 @@ |> Thm.close_derivation) goals cTs dtor_unfold_thms map_comp's map_cong0s; in - map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps + map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps end; val map_comp_thms =