src/HOL/Tools/BNF/bnf_lfp_size.ML
changeset 62690 c4fad0569a24
parent 62536 656e9653c645
child 63170 eae6549dbea2
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 22 08:00:15 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 22 08:00:33 2016 +0100
     1.3 @@ -187,8 +187,7 @@
     1.4              fold_map mk_size_of_arg xs []
     1.5              |>> remove (op =) HOLogic.zero;
     1.6            val sum =
     1.7 -            if null summands then base_case
     1.8 -            else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
     1.9 +            if null summands then base_case else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
    1.10          in
    1.11            append size_gen_o_mapss
    1.12            #> pair (fold_rev Term.lambda (map substCnatT xs) sum)
    1.13 @@ -313,7 +312,8 @@
    1.14        val maps0 = map map_of_bnf fp_bnfs;
    1.15  
    1.16        val size_gen_o_map_thmss =
    1.17 -        if live = 0 then replicate nn []
    1.18 +        if live = 0 then
    1.19 +          replicate nn []
    1.20          else
    1.21            let
    1.22              val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
    1.23 @@ -337,7 +337,7 @@
    1.24                  curry HOLogic.mk_eq) size_gen_o_map_lhss size_gen_o_map_rhss;
    1.25  
    1.26              val rec_o_maps =
    1.27 -              fold_rev (curry (op @) o (#co_rec_o_maps o #fp_co_induct_sugar)) fp_sugars [];
    1.28 +              fold_rev (curry (op @) o #co_rec_o_maps o #fp_co_induct_sugar) fp_sugars [];
    1.29  
    1.30              val size_gen_o_map_thmss =
    1.31                if nested_size_gen_o_maps_complete then