changeset 52659 | 58b87aa4dc3b |
parent 52368 | 13ca6876f748 |
child 52788 | da1fdbfebd39 |
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Jul 15 14:23:51 2013 +0200 @@ -1174,7 +1174,7 @@ end; val sumEN_thm' = - unfold_thms lthy @{thms all_unit_eq} + unfold_thms lthy @{thms unit_all_eq1} (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) [] (mk_sumEN_balanced n)) |> Morphism.thm phi;