renamed "mk_UnN" to "mk_UnIN"

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
@@ -499,6 +499,7 @@
         ((wrap, define_iter_likes), lthy')
       end;
 
+    (* TODO: remove all "nested" and "nesting" BNFs from pre_bnfs, if they're there *)
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     val nesting_map_ids = map map_id_of_bnf nesting_bnfs;

--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
@@ -206,7 +206,7 @@
 fun mk_set_hset_incl_hset_tac n defs rec_Suc i =
   EVERY' (map (TRY oo stac) defs @
     map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2,
-      mk_UnN n i] @
+      mk_UnIN n i] @
     [etac @{thm UN_I}, atac]) 1;
 
 fun mk_set_incl_hin_tac incls =
@@ -535,7 +535,7 @@
       hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
       rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
       CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
-        [rtac (mk_UnN n i), dtac (def RS subst_id),
+        [rtac (mk_UnIN n i), dtac (def RS subst_id),
         REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI,
         REPEAT_DETERM_N m o (rtac conjI THEN' atac),
         CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans,
@@ -678,7 +678,7 @@
               rtac Lev_0, rtac @{thm singletonI},
               REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
-              rtac Lev_Suc, rtac (mk_UnN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
+              rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
               rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
               etac mp, etac conjI, atac]) ks])
       (Lev_0s ~~ Lev_Sucs)] 1
@@ -753,7 +753,7 @@
             then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
               CONJ_WRAP' (fn (i'', Lev_0'') =>
                 EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
-                  rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i''),
+                  rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
                   rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
                   etac conjI, rtac (Lev_0'' RS equalityD2 RS set_mp),
                   rtac @{thm singletonI}])
@@ -770,7 +770,7 @@
                 CONJ_WRAP' (fn i' => rtac impI THEN'
                   CONJ_WRAP' (fn i'' =>
                     EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
-                      rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnN n i),
+                      rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnIN n i),
                       rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl,
                       rtac conjI, atac, dtac (sym RS trans RS sym),
                       rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans),
@@ -972,7 +972,7 @@
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
             rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
-            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI,
+            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
             rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
             rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI,
@@ -986,7 +986,7 @@
                   atac, atac, hyp_subst_tac, atac]
                 else etac (mk_InN_not_InM i' i'' RS notE)])
             (rev ks),
-            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnN n i'), rtac CollectI,
+            rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
             CONVERSION (Conv.top_conv
               (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
@@ -1196,7 +1196,7 @@
     REPEAT_DETERM_N n o rtac @{thm Un_upper1},
     REPEAT_DETERM_N n o
       EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
-        EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnN n i), etac @{thm UN_I},
+        EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
           etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
           EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
       (1 upto n) set_hsets set_hset_hsetss)] 1;

--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 14 12:09:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 14 12:09:27 2012 +0200
@@ -111,7 +111,7 @@
   val mk_nthI: int -> int -> thm
   val mk_nth_conv: int -> int -> thm
   val mk_ordLeq_csum: int -> int -> thm -> thm
-  val mk_UnN: int -> int -> thm
+  val mk_UnIN: int -> int -> thm
 
   val ctrans: thm
   val o_apply: thm
@@ -542,12 +542,12 @@
 end;
 
 local
-  fun mk_UnN' 0 = @{thm UnI2}
-    | mk_UnN' m = mk_UnN' (m - 1) RS @{thm UnI1};
+  fun mk_UnIN' 0 = @{thm UnI2}
+    | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1};
 in
-  fun mk_UnN 1 1 = @{thm TrueE[OF TrueI]}
-    | mk_UnN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1})
-    | mk_UnN n m = mk_UnN' (n - m)
+  fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]}
+    | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1})
+    | mk_UnIN n m = mk_UnIN' (n - m)
 end;
 
 fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);