--- 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);