# HG changeset patch
# User blanchet
# Date 1458630033 -3600
# Node ID c4fad0569a246397324df4cfc8eff9fecf27b1b8
# Parent  9b8b3db6ac03fdb5af6bb8e716d8cd4be135f1ef
nicer error

diff -r 9b8b3db6ac03 -r c4fad0569a24 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 22 08:00:15 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 22 08:00:33 2016 +0100
@@ -187,8 +187,7 @@
             fold_map mk_size_of_arg xs []
             |>> remove (op =) HOLogic.zero;
           val sum =
-            if null summands then base_case
-            else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
+            if null summands then base_case else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
         in
           append size_gen_o_mapss
           #> pair (fold_rev Term.lambda (map substCnatT xs) sum)
@@ -313,7 +312,8 @@
       val maps0 = map map_of_bnf fp_bnfs;
 
       val size_gen_o_map_thmss =
-        if live = 0 then replicate nn []
+        if live = 0 then
+          replicate nn []
         else
           let
             val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
@@ -337,7 +337,7 @@
                 curry HOLogic.mk_eq) size_gen_o_map_lhss size_gen_o_map_rhss;
 
             val rec_o_maps =
-              fold_rev (curry (op @) o (#co_rec_o_maps o #fp_co_induct_sugar)) fp_sugars [];
+              fold_rev (curry (op @) o #co_rec_o_maps o #fp_co_induct_sugar) fp_sugars [];
 
             val size_gen_o_map_thmss =
               if nested_size_gen_o_maps_complete then
diff -r 9b8b3db6ac03 -r c4fad0569a24 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Mar 22 08:00:15 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Mar 22 08:00:33 2016 +0100
@@ -61,6 +61,9 @@
     val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar);
     val alpha0s = map (TFree o snd) specs;
 
+    val _ = length tvs = length alpha0s orelse
+      error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name);
+
     (* instantiate the new type variables newtvs to oldtvs *)
     val subst = subst_TVars (tvs ~~ alpha0s);
     val typ_subst = typ_subst_TVars (tvs ~~ alpha0s);