# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID a452de24a877d187c923814c91d50c766a4bd243
# Parent  4e5ddf3162ac2cc09337c0b131c057feddec2062
tuned names

diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -24,8 +24,7 @@
   ordIso2 (infix "=o" 50) and
   csum (infixr "+c" 65) and
   cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90) and
-  convol ("<_ , _>")
+  cexp (infixr "^c" 90)
 
 no_syntax (xsymbols)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -302,8 +302,8 @@
 
     fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp0_tac {context = ctxt, prems = _} =
-      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
-      rtac refl 1;
+      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
+        @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
     fun map_cong0_tac {context = ctxt, prems = _} =
       mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
     val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_of_bnf bnf));
@@ -394,8 +394,8 @@
 
     fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp0_tac {context = ctxt, prems = _} =
-      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
-      rtac refl 1;
+      unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) ::
+        @{thms comp_assoc id_comp comp_id}) THEN rtac refl 1;
     fun map_cong0_tac {context = ctxt, prems = _} =
       rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
     val set_map0_tacs =
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_comp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -44,8 +44,8 @@
 
 val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
 val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
+val comp_eq_dest_lhs = @{thm comp_eq_dest_lhs};
 val csum_Cnotzero1 = @{thm csum_Cnotzero1};
-val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
 val trans_o_apply = @{thm trans[OF o_apply]};
 
@@ -54,7 +54,7 @@
 (* Composition *)
 
 fun mk_comp_set_alt_tac ctxt collect_set_map =
-  unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
+  unfold_thms_tac ctxt @{thms comp_assoc} THEN
   unfold_thms_tac ctxt [collect_set_map RS sym] THEN
   rtac refl 1;
 
@@ -64,7 +64,7 @@
 
 fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
   EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
-    rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
+    rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans), rtac Gmap_cong0] @
     map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
 
 fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
@@ -72,14 +72,14 @@
     replicate 3 (rtac trans_o_apply) @
     [rtac (arg_cong_Union RS trans),
      rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
-     rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans),
+     rtac (Gmap_comp0 RS sym RS comp_eq_dest_lhs RS trans),
      rtac Gmap_cong0] @
      map (fn thm => rtac (thm RS fun_cong)) set_map0s @
-     [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
+     [rtac (Gset_map0 RS comp_eq_dest_lhs), rtac sym, rtac trans_o_apply,
      rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
-     rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
+     rtac (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
      rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
-     rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
+     rtac @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
      rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
      [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
         rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -47,7 +47,7 @@
 val conversep_shift = @{thm conversep_le_swap} RS iffD1;
 
 fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
-fun mk_map_comp comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
+fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp];
 fun mk_map_cong_tac ctxt cong0 =
   (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
    REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
@@ -61,7 +61,7 @@
   (etac subset_trans THEN' atac) 1;
 
 fun mk_collect_set_map_tac set_map0s =
-  (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
+  (rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
   EVERY' (map (fn set_map0 =>
     rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
     rtac set_map0) set_map0s) THEN'
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -332,8 +332,8 @@
         val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
         val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
         val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
-        val fold_thms = fp_case fp @{thm o_assoc[symmetric]} @{thm o_assoc} ::
-          @{thms id_apply o_apply o_id id_o map_pair.comp map_pair.id sum_map.comp sum_map.id};
+        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
+          o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
         val rec_thms = fold_thms @ fp_case fp
           @{thms fst_convol map_pair_o_convol convol_o}
           @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_fp_util.ML
--- 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;
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -1969,14 +1969,14 @@
 
     val map_id0s_o_id =
       map (fn thm =>
-        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_o})
+        mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp})
       map_id0s;
 
     val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
       `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
-        |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
-           map_id0s_o_id @ sym_map_comps)
+        |> Local_Defs.unfold lthy (@{thms o_sum_case comp_id id_comp comp_assoc[symmetric]
+           sum_case_o_inj(1)} @ map_id0s_o_id @ sym_map_comps)
         OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
 
     val timer = time (timer "corec definitions & thms");
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -137,7 +137,7 @@
     Splitter.split_tac (split_if :: splits) ORELSE'
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
-    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def o_def split_def
+    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
        sum.cases} @ mapsx @ map_comps @ map_idents)))));
 
 fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -247,7 +247,7 @@
         EVERY' (map (fn thm =>
           EVERY' [rtac @{thm GrpI},
             rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
-            REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
+            REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), atac,
             REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
             CONJ_WRAP' (fn (i, thm) =>
               if i <= m
@@ -267,11 +267,11 @@
           @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
         hyp_subst_tac ctxt,
         rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
-        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
-        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
+        REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
+        REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
         atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
-        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
-        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
+        REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
+        REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
         rtac trans, rtac map_cong0,
         REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
@@ -983,8 +983,8 @@
 fun mk_map_tac m n cT unfold map_comp map_cong0 =
   EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
     rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
-    REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
-    REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
+    REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
+    REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
     rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
 
 fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
@@ -1010,9 +1010,10 @@
   EVERY' [rtac map_unique,
     EVERY' (map2 (fn map_thm => fn map_comp0 =>
       EVERY' (map rtac
-        [@{thm o_assoc} RS trans,
+        [@{thm comp_assoc[symmetric]} RS trans,
         @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
-        @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
+        @{thm comp_assoc[symmetric]} RS sym RS trans, map_thm RS arg_cong RS trans,
+        @{thm comp_assoc[symmetric]} RS trans,
         @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]]))
     maps map_comp0s)] 1;
 
@@ -1053,7 +1054,7 @@
 
 fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt =
   rtac unfold_unique 1 THEN
-  unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
+  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc[symmetric] id_comp comp_id}) THEN
   ALLGOALS (etac sym);
 
 fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss
@@ -1157,7 +1158,7 @@
         (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
-          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
+          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
           rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
         @{thms fst_conv snd_conv}];
@@ -1187,7 +1188,7 @@
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
           rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
-          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
+          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
             REPEAT_DETERM o
@@ -1212,10 +1213,11 @@
           rtac exI, rtac conjI, rtac conjI,
           rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym),
           rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]),
-          REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]},
+          REPEAT_DETERM_N m o
+            rtac @{thm trans[OF fun_cong[OF comp_id] sym[OF fun_cong[OF id_comp]]]},
           REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
           rtac (map_comp0 RS trans), rtac (map_cong RS trans),
-          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]},
+          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_comp]},
           REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
           etac (@{thm prod.cases} RS map_arg_cong RS trans),
           SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), 
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -1313,7 +1313,7 @@
     val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
       `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
-        |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @
+        |> Local_Defs.unfold lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @
            map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
 
     val timer = time (timer "rec definitions & thms");
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -461,7 +461,8 @@
 fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
   unfold_thms_tac ctxt fun_defs THEN
   HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
-  unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
+  unfold_thms_tac ctxt (@{thms id_def split comp_def fst_conv snd_conv} @ map_comps @
+    map_idents) THEN
   HEADGOAL (rtac refl);
 
 fun prepare_primrec fixes specs lthy =
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -404,7 +404,7 @@
           EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
             etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]];
   in
-    (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm o_id}) THEN'
+    (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}) THEN'
     rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
     stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN'
     stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1
@@ -585,7 +585,7 @@
 
 fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt =
   rtac fold_unique 1 THEN
-  unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN
+  unfold_thms_tac ctxt (sym_map_comps @ @{thms comp_assoc id_comp comp_id}) THEN
   ALLGOALS atac;
 
 fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
@@ -675,7 +675,7 @@
 fun mk_map_id0_tac map_id0s unique =
   (rtac sym THEN' rtac unique THEN'
   EVERY' (map (fn thm =>
-    EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
+    EVERY' [rtac trans, rtac @{thm id_comp}, rtac trans, rtac sym, rtac @{thm comp_id},
       rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
 
 fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 =
@@ -737,7 +737,7 @@
         (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
-          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
+          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
           rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
           etac eq_arg_cong_ctor_dtor])
@@ -766,7 +766,7 @@
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
           rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
-          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
+          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
             REPEAT_DETERM o
diff -r 4e5ddf3162ac -r a452de24a877 src/HOL/Tools/BNF/bnf_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Mon Jan 20 18:24:56 2014 +0100
@@ -58,7 +58,7 @@
 
 fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
 fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
-  (Abs_inj_thm RS @{thm bijI});
+  (Abs_inj_thm RS @{thm bijI'});
 
 
 
@@ -95,7 +95,7 @@
   rtac refl 1;
 
 fun mk_map_comp_id_tac map_comp0 =
-  (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
+  (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1;
 
 fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
   EVERY' [rtac mp, rtac map_cong0,