changeset 49161 | a8e74375d971 |
parent 49157 | 6407346b74c7 |
child 49165 | c6ccaf6df93c |
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 15:40:28 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 15:40:29 2012 +0200 @@ -195,7 +195,7 @@ (Drule.instantiate' (map (SOME o certifyT lthy) prod_Ts) [] (mk_sumEN n)) |> Morphism.thm phi; in - mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm' + mk_exhaust_tac ctxt n ctr_defs fld_iff_unf_thm sumEN_thm' end; val inject_tacss =