1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
     1.5  
     1.6  fun tuple_fun Ts (xi, T) =
     1.7 -  Library.funpow (length Ts) HOLogic.mk_split
     1.8 +  Library.funpow (length Ts) HOLogic.mk_case_prod
     1.9      (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
    1.10  
    1.11  fun split_all_tuples ctxt =