changeset 54917 | a426e38a8a7e |
parent 54913 | 7b18c41df27a |
child 54921 | 862c36b6e57c |
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 20:25:40 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 20:51:09 2014 +0100 @@ -1208,7 +1208,7 @@ [] else mk_primcorec_disc_iff_tac lthy (the_single exhaust_thms) (the_single disc_thms) - (flat disc_thmss) (flat disc_excludess) + disc_thmss (flat disc_excludess) |> K |> Goal.prove lthy [] [] goal |> Thm.close_derivation |> single