nicer error
authorblanchet
Tue Mar 22 08:00:33 2016 +0100 (2016-03-22)
changeset 62690c4fad0569a24
parent 62689 9b8b3db6ac03
child 62691 9bfcbab7cd99
nicer error
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/BNF/bnf_lift.ML
     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
     2.1 --- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Mar 22 08:00:15 2016 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Mar 22 08:00:33 2016 +0100
     2.3 @@ -61,6 +61,9 @@
     2.4      val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar);
     2.5      val alpha0s = map (TFree o snd) specs;
     2.6  
     2.7 +    val _ = length tvs = length alpha0s orelse
     2.8 +      error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name);
     2.9 +
    2.10      (* instantiate the new type variables newtvs to oldtvs *)
    2.11      val subst = subst_TVars (tvs ~~ alpha0s);
    2.12      val typ_subst = typ_subst_TVars (tvs ~~ alpha0s);