--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Oct 13 09:21:15 2015 +0200
@@ -298,7 +298,7 @@
| (_, branches') =>
Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
branches'))
- | (c as Const (@{const_name uncurry}, _), arg :: args) =>
+ | (c as Const (@{const_name case_prod}, _), arg :: args) =>
massage_rec bound_Ts
(unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
| (Const (c, _), args as _ :: _ :: _) =>
@@ -402,12 +402,12 @@
end
| NONE =>
(case t of
- Const (@{const_name uncurry}, _) $ t' =>
+ Const (@{const_name case_prod}, _) $ t' =>
let
val U' = curried_type U;
val T' = curried_type T;
in
- Const (@{const_name uncurry}, U' --> U) $ massage_any_call bound_Ts U' T' t'
+ Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
end
| t1 $ t2 =>
(if has_call t2 then
@@ -931,9 +931,9 @@
let val (u, vs) = strip_comb t in
if is_Free u andalso has_call u then
Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs
- else if try (fst o dest_Const) u = SOME @{const_name uncurry} then
+ else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
map (rewrite bound_Ts) vs |> chop 1
- |>> HOLogic.mk_split o the_single
+ |>> HOLogic.mk_case_prod o the_single
|> Term.list_comb
else
Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)