--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 20 18:24:56 2014 +0100
@@ -534,14 +534,14 @@
val n = length sym_map_comps;
val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
- val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_o} @{thm o_id} RS fun_cong);
+ val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
val map_cong_active_args1 = replicate n (if is_rec
then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong
else refl);
- val map_cong_passive_args2 = replicate m (fp_case fp @{thm o_id} @{thm id_o} RS fun_cong);
+ val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
val map_cong_active_args2 = replicate n (if is_rec
then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id}
- else fp_case fp @{thm id_o} @{thm o_id} RS fun_cong);
+ else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;