src/HOL/BNF/Tools/bnf_comp.ML

--- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -149,9 +149,9 @@
     (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
     val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
 
-    fun map_id_tac _ =
-      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong0_of_bnf outer)
-        (map map_id_of_bnf inners);
+    fun map_id0_tac _ =
+      mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
+        (map map_id0_of_bnf inners);
 
     fun map_comp_tac _ =
       mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
@@ -233,7 +233,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -300,7 +300,7 @@
     val bd = mk_cprod
       (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
 
-    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp_tac {context = ctxt, prems = _} =
       unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
@@ -339,7 +339,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -390,7 +390,7 @@
 
     val bd = mk_bd_of_bnf Ds As bnf;
 
-    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp_tac {context = ctxt, prems = _} =
       unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
@@ -424,7 +424,7 @@
 
     fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -474,7 +474,7 @@
 
     val bd = mk_bd_of_bnf Ds As bnf;
 
-    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 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);
@@ -497,7 +497,7 @@
 
     fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -630,7 +630,7 @@
       (rtac (unfold_all thm) THEN'
       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
 
-    val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+    val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
       (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
       (mk_tac (map_wpull_of_bnf bnf))