src/HOL/Tools/BNF/bnf_lift.ML
changeset 62690 c4fad0569a24
parent 62621 a1e73be79c0b
child 62777 596baa1a3251
     1.1 --- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Mar 22 08:00:15 2016 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Mar 22 08:00:33 2016 +0100
     1.3 @@ -61,6 +61,9 @@
     1.4      val tvs = AbsT |> dest_Type |> snd |> map (fst o dest_TVar);
     1.5      val alpha0s = map (TFree o snd) specs;
     1.6  
     1.7 +    val _ = length tvs = length alpha0s orelse
     1.8 +      error ("Expected " ^ string_of_int (length tvs) ^ " type argument(s) to " ^ quote AbsT_name);
     1.9 +
    1.10      (* instantiate the new type variables newtvs to oldtvs *)
    1.11      val subst = subst_TVars (tvs ~~ alpha0s);
    1.12      val typ_subst = typ_subst_TVars (tvs ~~ alpha0s);