1.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -146,11 +146,11 @@
     1.4  (* iterated versions. Nonstandard left-nested tuples arise naturally
     1.5  from "split o split o split"*)
     1.6  fun curry_n arity = funpow (arity - 1) mk_curry;
     1.7 -fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_split;
     1.8 +fun uncurry_n arity = funpow (arity - 1) HOLogic.mk_case_prod;
     1.9  
    1.10  val curry_uncurry_ss =
    1.11    simpset_of (put_simpset HOL_basic_ss @{context}
    1.12 -    addsimps [@{thm Product_Type.curry_split}, @{thm Product_Type.split_curry}])
    1.13 +    addsimps [@{thm Product_Type.curry_case_prod}, @{thm Product_Type.case_prod_curry}])
    1.14  
    1.15  val split_conv_ss =
    1.16    simpset_of (put_simpset HOL_basic_ss @{context}
    1.17 @@ -177,7 +177,7 @@
    1.18         THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
    1.19      |> (fn thm => thm OF [mono_thm, f_def])
    1.20      |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
    1.21 -         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_split}]))
    1.22 +         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
    1.23      |> singleton (Variable.export ctxt' ctxt)
    1.24    end
    1.25