src/HOL/Tools/BNF/bnf_lift.ML

     val zip_closed_F = Logic.all var_z imp_zip;
 
     (* val wit_closed_F = @{term "wit_F a \<in> F"}; *)
     val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy;
     val (var_bs, _) = mk_Frees "a" alphas names_lthy;
+    fun binder_types_until_eq V T =
+      let
+        fun strip (TU as Type ("fun", [T, U])) = if V = TU then [] else T :: strip U
+          | strip T = if V = T then [] else
+              error ("Bad type for witness: " ^ quote (Syntax.string_of_typ lthy T));
+      in strip T end;
     val Iwits = the_default wits_F (Option.map (map (`(map (fn T =>
-      find_index (fn U => T = U) alphas) o fst o strip_type o fastype_of))) wits);
+      find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits);
     val wit_closed_Fs =
       Iwits |> map (fn (I, wit_F) =>
         let
           val vars = map (nth var_as) I;
           val wit_a = list_comb (wit_F, vars);