--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Feb 12 08:35:57 2014 +0100
@@ -195,7 +195,7 @@
let val branches' = map (massage_rec bound_Ts) branches in
Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
end
- | (c as Const (@{const_name prod_case}, _), arg :: args) =>
+ | (c as Const (@{const_name case_prod}, _), arg :: args) =>
massage_rec bound_Ts
(unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
| (Const (c, _), args as _ :: _ :: _) =>
@@ -295,12 +295,12 @@
end
| NONE =>
(case t of
- Const (@{const_name prod_case}, _) $ t' =>
+ Const (@{const_name case_prod}, _) $ t' =>
let
val U' = curried_type U;
val T' = curried_type T;
in
- Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
+ Const (@{const_name case_prod}, U' --> U) $ massage_call bound_Ts U' T' t'
end
| t1 $ t2 =>
(if has_call t2 then
@@ -771,7 +771,7 @@
let val (u, vs) = strip_comb t in
if is_Free u andalso has_call u then
Inr_const U T $ mk_tuple1 bound_Ts vs
- else if try (fst o dest_Const) u = SOME @{const_name prod_case} 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
|> Term.list_comb