--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Sep 06 22:14:51 2015 +0200
@@ -294,7 +294,7 @@
| (_, branches') =>
Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
branches'))
- | (c as Const (@{const_name case_prod}, _), arg :: args) =>
+ | (c as Const (@{const_name uncurry}, _), arg :: args) =>
massage_rec bound_Ts
(unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
| (Const (c, _), args as _ :: _ :: _) =>
@@ -398,12 +398,12 @@
end
| NONE =>
(case t of
- Const (@{const_name case_prod}, _) $ t' =>
+ Const (@{const_name uncurry}, _) $ t' =>
let
val U' = curried_type U;
val T' = curried_type T;
in
- Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
+ Const (@{const_name uncurry}, U' --> U) $ massage_any_call bound_Ts U' T' t'
end
| t1 $ t2 =>
(if has_call t2 then
@@ -927,7 +927,7 @@
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 case_prod} then
+ else if try (fst o dest_Const) u = SOME @{const_name uncurry} then
map (rewrite bound_Ts) vs |> chop 1
|>> HOLogic.mk_split o the_single
|> Term.list_comb