# HG changeset patch
# User traytel
# Date 1392731486 -3600
# Node ID fd9ea8ae28f6c1c72740a66b08a670bb17363c56
# Parent  892a425c5eaae76a470dbe9caeb5f999cc9bcbb3
syntactic simplifications of internal (co)datatype constructions

diff -r 892a425c5eaa -r fd9ea8ae28f6 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Feb 18 14:51:26 2014 +0100
@@ -163,8 +163,8 @@
      HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys;
     val hrecTs = map fastype_of Zeros;
 
-    val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
-      As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
+    val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
+      Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
       self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
       (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy
       |> mk_Frees' "b" activeAs
@@ -172,7 +172,6 @@
       ||>> mk_Frees "b" activeAs
       ||>> mk_Frees "b" activeBs
       ||>> mk_Frees' "y" passiveAs
-      ||>> mk_Frees "A" ATs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B'" B'Ts
@@ -203,7 +202,7 @@
       ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs);
 
     val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
-    val passive_Id_ons = map mk_Id_on As;
+    val passive_eqs = map HOLogic.eq_const passiveAs;
     val active_UNIVs = map HOLogic.mk_UNIV activeAs;
     val sum_UNIVs = map HOLogic.mk_UNIV sumBsAs;
     val passive_ids = map HOLogic.id_const passiveAs;
@@ -297,16 +296,16 @@
     val coalg_bind = mk_internal_b (coN ^ algN) ;
     val coalg_def_bind = (Thm.def_binding coalg_bind, []);
 
-    (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in A1 .. Am B1 ... Bn)*)
+    (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in UNIV .. UNIV B1 ... Bn)*)
     val coalg_spec =
       let
-        val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
+        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
         fun mk_coalg_conjunct B s X z z' =
           mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));
 
         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
+        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
       end;
 
     val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
@@ -316,44 +315,44 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
-    val coalg_def = mk_unabs_def (live + n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
-
-    fun mk_coalg As Bs ss =
+    val coalg_def = mk_unabs_def (2 * n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
+
+    fun mk_coalg Bs ss =
       let
-        val args = As @ Bs @ ss;
+        val args = Bs @ ss;
         val Ts = map fastype_of args;
         val coalgT = Library.foldr (op -->) (Ts, HOLogic.boolT);
       in
         Term.list_comb (Const (coalg, coalgT), args)
       end;
 
-    val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
+    val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
 
     val coalg_in_thms = map (fn i =>
       coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
 
     val coalg_set_thmss =
       let
-        val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
+        val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
         fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
         fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
         val prems = map2 mk_prem zs Bs;
-        val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) (As @ Bs) sets)
+        val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
           ss zs setssAs;
         val goalss = map3 (fn x => fn prem => fn concls => map (fn concl =>
-          fold_rev Logic.all (x :: As @ Bs @ ss)
+          fold_rev Logic.all (x :: Bs @ ss)
             (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
       in
         map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal
           (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
       end;
 
-    fun mk_tcoalg ATs BTs = mk_coalg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
+    fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);
 
     val tcoalg_thm =
       let
         val goal = fold_rev Logic.all ss
-          (HOLogic.mk_Trueprop (mk_tcoalg passiveAs activeAs ss))
+          (HOLogic.mk_Trueprop (mk_tcoalg activeAs ss))
       in
         Goal.prove_sorry lthy [] [] goal
           (K (stac coalg_def 1 THEN CONJ_WRAP
@@ -719,8 +718,8 @@
         fun mk_bis R s s' b1 b2 RF map1 map2 sets =
           list_all_free [b1, b2] (HOLogic.mk_imp
             (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
-            mk_Bex (mk_in (As @ Rs) sets (snd (dest_Free RF))) (Term.absfree (dest_Free RF)
-              (HOLogic.mk_conj
+            mk_Bex (mk_in (passive_UNIVs @ Rs) sets (snd (dest_Free RF)))
+              (Term.absfree (dest_Free RF) (HOLogic.mk_conj
                 (HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1),
                 HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2))))));
 
@@ -728,7 +727,7 @@
           (bis_le, Library.foldr1 HOLogic.mk_conj
             (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss @ B's @ s's @ Rs) rhs
+        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs
       end;
 
     val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
@@ -738,11 +737,11 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
-    val bis_def = mk_unabs_def (m + 5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
-
-    fun mk_bis As Bs1 ss1 Bs2 ss2 Rs =
+    val bis_def = mk_unabs_def (5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
+
+    fun mk_bis Bs1 ss1 Bs2 ss2 Rs =
       let
-        val args = As @ Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
+        val args = Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
         val Ts = map fastype_of args;
         val bisT = Library.foldr (op -->) (Ts, HOLogic.boolT);
       in
@@ -752,11 +751,11 @@
     val bis_cong_thm =
       let
         val prems = map HOLogic.mk_Trueprop
-         (mk_bis As Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
-        val concl = HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs_copy);
+         (mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
+        val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
             (Logic.list_implies (prems, concl)))
           (K ((hyp_subst_tac lthy THEN' atac) 1))
         |> Thm.close_derivation
@@ -767,38 +766,38 @@
         fun mk_conjunct R s s' b1 b2 rel =
           list_all_free [b1, b2] (HOLogic.mk_imp
             (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
-            Term.list_comb (rel, map mk_in_rel (passive_Id_ons @ Rs)) $ (s $ b1) $ (s' $ b2)));
+            Term.list_comb (rel, passive_eqs @ map mk_in_rel Rs) $ (s $ b1) $ (s' $ b2)));
 
         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
             (map6 mk_conjunct Rs ss s's zs z's relsAsBs))
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
-            (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
+            (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)))
           (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss))
         |> Thm.close_derivation
       end;
 
     val bis_converse_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
+        (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
           (Logic.mk_implies
-            (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
-            HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
+            (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+            HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs)))))
         (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
       |> Thm.close_derivation;
 
     val bis_O_thm =
       let
         val prems =
-          [HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
-           HOLogic.mk_Trueprop (mk_bis As B's s's B''s s''s R's)];
+          [HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+           HOLogic.mk_Trueprop (mk_bis B's s's B''s s''s R's)];
         val concl =
-          HOLogic.mk_Trueprop (mk_bis As Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
+          HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
             (Logic.list_implies (prems, concl)))
           (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
         |> Thm.close_derivation
@@ -807,10 +806,10 @@
     val bis_Gr_thm =
       let
         val concl =
-          HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map2 mk_Gr Bs fs));
+          HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([coalg_prem, mor_prem], concl)))
           (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
             morE_thms coalg_in_thms)
@@ -828,12 +827,12 @@
       let
         val prem =
           HOLogic.mk_Trueprop (mk_Ball Idx
-            (Term.absfree idx' (mk_bis As Bs ss B's s's (map (fn R => R $ idx) Ris))));
+            (Term.absfree idx' (mk_bis Bs ss B's s's (map (fn R => R $ idx) Ris))));
         val concl =
-          HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map (mk_UNION Idx) Ris));
+          HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
+          (fold_rev Logic.all (Idx :: Bs @ ss @ B's @ s's @ Ris)
             (Logic.mk_implies (prem, concl)))
           (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
         |> Thm.close_derivation
@@ -841,9 +840,9 @@
 
     (* self-bisimulation *)
 
-    fun mk_sbis As Bs ss Rs = mk_bis As Bs ss Bs ss Rs;
-
-    val sbis_prem = HOLogic.mk_Trueprop (mk_sbis As Bs ss sRs);
+    fun mk_sbis Bs ss Rs = mk_bis Bs ss Bs ss Rs;
+
+    val sbis_prem = HOLogic.mk_Trueprop (mk_sbis Bs ss sRs);
 
     (* largest self-bisimulation *)
 
@@ -852,10 +851,10 @@
     val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;
 
     val all_sbis = HOLogic.mk_Collect (fst Rtuple', snd Rtuple', list_exists_free sRs
-      (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis As Bs ss sRs)));
+      (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis Bs ss sRs)));
 
     fun lsbis_spec i =
-      fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss)
+      fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss)
         (mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i)));
 
     val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
@@ -868,12 +867,12 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val lsbis_defs = map (fn def =>
-      mk_unabs_def (live + n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
+      mk_unabs_def (2 * n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
     val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees;
 
-    fun mk_lsbis As Bs ss i =
+    fun mk_lsbis Bs ss i =
       let
-        val args = As @ Bs @ ss;
+        val args = Bs @ ss;
         val Ts = map fastype_of args;
         val RT = mk_relT (`I (HOLogic.dest_setT (fastype_of (nth Bs (i - 1)))));
         val lsbisT = Library.foldr (op -->) (Ts, RT);
@@ -883,8 +882,8 @@
 
     val sbis_lsbis_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (As @ Bs @ ss)
-          (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
+        (fold_rev Logic.all (Bs @ ss)
+          (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks))))
         (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
       |> Thm.close_derivation;
 
@@ -895,8 +894,8 @@
 
     val incl_lsbis_thms =
       let
-        fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis As Bs ss i));
-        val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs)
+        fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
+        val goals = map2 (fn i => fn R => fold_rev Logic.all (Bs @ ss @ sRs)
           (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
       in
         map3 (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal
@@ -905,8 +904,8 @@
 
     val equiv_lsbis_thms =
       let
-        fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis As Bs ss i));
-        val goals = map2 (fn i => fn B => fold_rev Logic.all (As @ Bs @ ss)
+        fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
+        val goals = map2 (fn i => fn B => fold_rev Logic.all (Bs @ ss)
           (Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs;
       in
         map3 (fn goal => fn l_incl => fn incl_l =>
@@ -1033,7 +1032,7 @@
     val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
 
     val isNodeT =
-      Library.foldr (op -->) (map fastype_of (As @ [Kl, lab, kl]), HOLogic.boolT);
+      Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT);
 
     val Succs = map3 (fn i => fn k => fn k' =>
       HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl)))
@@ -1041,12 +1040,12 @@
 
     fun isNode_spec sets x i =
       let
-        val (passive_sets, active_sets) = chop m (map (fn set => set $ x) sets);
+        val active_sets = drop m (map (fn set => set $ x) sets);
         val rhs = list_exists_free [x]
           (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
-          map2 mk_leq passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
+          map2 (curry HOLogic.mk_eq) active_sets Succs));
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ [Kl, lab, kl]) rhs
+        fold_rev (Term.absfree o Term.dest_Free) [Kl, lab, kl] rhs
       end;
 
     val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
@@ -1060,11 +1059,11 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val isNode_defs = map (fn def =>
-      mk_unabs_def (m + 3) (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
+      mk_unabs_def 3 (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
     val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees;
 
-    fun mk_isNode As kl i =
-      Term.list_comb (Const (nth isNodes (i - 1), isNodeT), As @ [Kl, lab, kl]);
+    fun mk_isNode kl i =
+      Term.list_comb (Const (nth isNodes (i - 1), isNodeT), [Kl, lab, kl]);
 
     val isTree =
       let
@@ -1074,9 +1073,9 @@
 
         val tree = mk_Ball Kl (Term.absfree kl'
           (HOLogic.mk_conj
-            (Library.foldr1 HOLogic.mk_disj (map (mk_isNode As kl) ks),
+            (Library.foldr1 HOLogic.mk_disj (map (mk_isNode kl) ks),
             Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' =>
-              mk_Ball Succ (Term.absfree k' (mk_isNode As
+              mk_Ball Succ (Term.absfree k' (mk_isNode
                 (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
             Succs ks kks kks'))));
 
@@ -1092,13 +1091,9 @@
     val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
 
     fun carT_spec i =
-      let
-        val rhs = HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
-          (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
-            HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
-      in
-        fold_rev (Term.absfree o Term.dest_Free) As rhs
-      end;
+      HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
+        (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
+          HOLogic.mk_conj (isTree, mk_isNode (HOLogic.mk_list sum_sbdT []) i))));
 
     val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
       lthy
@@ -1109,13 +1104,10 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
-    val carT_defs = map (fn def =>
-      mk_unabs_def m (Morphism.thm phi def RS meta_eq_to_obj_eq)) carT_def_frees;
+    val carT_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) carT_def_frees;
     val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees;
 
-    fun mk_carT As i = Term.list_comb
-      (Const (nth carTs (i - 1),
-         Library.foldr (op -->) (map fastype_of As, HOLogic.mk_setT treeT)), As);
+    fun mk_carT i = Const (nth carTs (i - 1), HOLogic.mk_setT treeT);
 
     val strT_binds = mk_internal_bs strTN;
     fun strT_bind i = nth strT_binds (i - 1);
@@ -1152,12 +1144,11 @@
 
     fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
 
-    val carTAs = map (mk_carT As) ks;
+    val carTAs = map mk_carT ks;
     val strTAs = map2 mk_strT treeFTs ks;
 
     val coalgT_thm =
-      Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
+      Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs))
         (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
           (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
       |> Thm.close_derivation;
@@ -1405,36 +1396,6 @@
         map (fn i => map (fn i' => rv_last' RS mk_conjunctN n i RS mk_conjunctN n i') ks) ks
       end;
 
-    val set_rv_Lev_thmsss = if m = 0 then replicate n (replicate n []) else
-      let
-        fun mk_case s sets z z_free = Term.absfree z_free (Library.foldr1 HOLogic.mk_conj
-          (map2 (fn set => fn A => mk_leq (set $ (s $ z)) A) (take m sets) As));
-
-        fun mk_conjunct i z B = HOLogic.mk_imp
-          (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
-          mk_case_sumN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
-
-        val goal = list_all_free (kl :: zs)
-          (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs));
-
-        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
-
-        val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
-            (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
-            (K (mk_set_rv_Lev_tac lthy m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
-              coalg_set_thmss from_to_sbd_thmss)))
-          |> Thm.close_derivation;
-
-        val set_rv_Lev' = mk_specN (n + 1) set_rv_Lev;
-      in
-        map (fn i => map (fn i' =>
-          split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
-            else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
-              (2, @{thm sum.weak_case_cong} RS iffD1) RS
-              (mk_sum_caseN n i' RS iffD1))) ks) ks
-      end;
-
     val set_Lev_thmsss =
       let
         fun mk_conjunct i z =
@@ -1514,29 +1475,25 @@
 
     val mor_beh_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
-          HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
+        (fold_rev Logic.all ss (HOLogic.mk_Trueprop
+          (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks))))
         (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
           beh_defs carT_defs strT_defs isNode_defs
           to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
-          length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
-          set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
-          set_mapss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
+          length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss set_Lev_thmsss
+          set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s map_arg_cong_thms)
       |> Thm.close_derivation;
 
     val timer = time (timer "Behavioral morphism");
 
-    fun mk_LSBIS As i = mk_lsbis As (map (mk_carT As) ks) strTAs i;
-    fun mk_car_final As i =
-      mk_quotient (mk_carT As i) (mk_LSBIS As i);
-    fun mk_str_final As i =
+    val lsbisAs = map (mk_lsbis carTAs strTAs) ks;
+
+    fun mk_str_final i =
       mk_univ (HOLogic.mk_comp (Term.list_comb (nth final_maps (i - 1),
-        passive_ids @ map (mk_proj o mk_LSBIS As) ks), nth strTAs (i - 1)));
-
-    val car_finalAs = map (mk_car_final As) ks;
-    val str_finalAs = map (mk_str_final As) ks;
-    val car_finals = map (mk_car_final passive_UNIVs) ks;
-    val str_finals = map (mk_str_final passive_UNIVs) ks;
+        passive_ids @ map mk_proj lsbisAs), nth strTAs (i - 1)));
+
+    val car_finals = map2 mk_quotient carTAs lsbisAs;
+    val str_finals = map mk_str_final ks;
 
     val coalgT_set_thmss = map (map (fn thm => coalgT_thm RS thm)) coalg_set_thmss;
     val equiv_LSBIS_thms = map (fn thm => coalgT_thm RS thm) equiv_lsbis_thms;
@@ -1544,11 +1501,10 @@
     val congruent_str_final_thms =
       let
         fun mk_goal R final_map strT =
-          fold_rev Logic.all As (HOLogic.mk_Trueprop
-            (mk_congruent R (HOLogic.mk_comp
-              (Term.list_comb (final_map, passive_ids @ map (mk_proj o mk_LSBIS As) ks), strT))));
-
-        val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
+          HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp
+            (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT)));
+
+        val goals = map3 mk_goal lsbisAs final_maps strTAs;
       in
         map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
@@ -1557,21 +1513,19 @@
         goals lsbisE_thms map_comp_id_thms map_cong0s
       end;
 
-    val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
-      (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs)))
+    val coalg_final_thm = Goal.prove_sorry lthy [] []
+      (HOLogic.mk_Trueprop (mk_coalg car_finals str_finals))
       (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
         set_mapss coalgT_set_thmss))
       |> Thm.close_derivation;
 
-    val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
-      (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs
-        (map (mk_proj o mk_LSBIS As) ks))))
+    val mor_T_final_thm = Goal.prove_sorry lthy [] []
+      (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
       (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms))
       |> Thm.close_derivation;
 
     val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
-    val in_car_final_thms = map (fn mor_image' => mor_image' OF
-      [tcoalg_thm RS mor_final_thm, UNIV_I]) mor_image'_thms;
+    val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
 
     val timer = time (timer "Final coalgebra");
 
@@ -1660,7 +1614,7 @@
         val mor_Rep =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
-            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m (mor_def :: dtor_defs) Reps
+            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps
               Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
           |> Thm.close_derivation;
 
@@ -1686,7 +1640,7 @@
       |> fold_map4 (fn i => fn abs => fn f => fn z =>
         Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
           ks Abs_Ts (map (fn i => HOLogic.mk_comp
-            (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs
+            (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
       |>> apsnd split_list o split_list
       ||> `Local_Theory.restore;
 
@@ -1706,8 +1660,7 @@
     val mor_unfold_thm =
       let
         val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
-        val morEs' = map (fn thm =>
-          (thm OF [tcoalg_thm RS mor_final_thm, UNIV_I]) RS sym) morE_thms;
+        val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all ss
@@ -1720,7 +1673,7 @@
 
     val (raw_coind_thms, raw_coind_thm) =
       let
-        val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs);
+        val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
         val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
@@ -1740,7 +1693,7 @@
           (map2 mk_fun_eq unfold_fs ks));
 
         val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
-        val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm];
+        val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
 
         val unique_mor = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
@@ -1925,7 +1878,7 @@
 
         fun mk_rel_prem phi dtor rel Jz Jz_copy =
           let
-            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $
+            val concl = Term.list_comb (rel, passive_eqs @ phis) $
               (dtor $ Jz) $ (dtor $ Jz_copy);
           in
             HOLogic.mk_Trueprop
diff -r 892a425c5eaa -r fd9ea8ae28f6 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Feb 18 14:51:26 2014 +0100
@@ -48,15 +48,14 @@
   val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
   val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
   val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
-  val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list list ->
+  val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
     thm list -> thm list -> tactic
   val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
   val mk_mor_UNIV_tac: thm list -> thm -> tactic
   val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
     thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
     thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
-    thm list list list -> thm list list list -> thm list list -> thm list list -> thm list ->
-    thm list -> thm list -> tactic
+    thm list list list -> thm list list -> thm list -> thm list -> thm list -> tactic
   val mk_mor_case_sum_tac: 'a list -> thm -> tactic
   val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
   val mk_mor_elim_tac: thm -> tactic
@@ -87,8 +86,6 @@
   val mk_set_ge_tac: int  -> thm -> thm list -> tactic
   val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   val mk_set_map0_tac: thm -> thm -> tactic
-  val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
-    thm list -> thm list -> thm list list -> thm list list -> tactic
   val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
@@ -108,8 +105,6 @@
 val nat_induct = @{thm nat_induct};
 val o_apply_trans_sym = o_apply RS trans RS sym;
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
-  @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
 val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
 val sum_weak_case_cong = @{thm sum.weak_case_cong};
@@ -117,10 +112,6 @@
 val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
 val rev_bspec = Drule.rotate_prems 1 bspec;
 val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
-val conversep_in_rel_Id_on =
-   @{thm trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]};
-val relcompp_in_rel_Id_on =
-   @{thm   trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]};
 val converse_shift = @{thm converse_subset_swap} RS iffD1;
 
 fun mk_coalg_set_tac coalg_def =
@@ -245,8 +236,8 @@
             CONJ_WRAP' (fn (i, thm) =>
               if i <= m
               then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
-                etac @{thm image_mono}, rtac @{thm image_subsetI},
-                etac @{thm Collect_split_in_relI[OF Id_onI]}]
+                etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
+                rtac @{thm case_prodI}, rtac refl]
               else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
                 rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
             (1 upto (m + n) ~~ set_map0s)])
@@ -266,13 +257,11 @@
         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 m o EVERY' [rtac @{thm Collect_splitD}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
         atac, rtac CollectI,
         CONJ_WRAP' (fn (i, thm) =>
-          if i <= m
-          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
-            rtac @{thm Id_on_fst}, etac set_mp, atac]
+          if i <= m then rtac subset_UNIV
           else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
             rtac trans_fun_cong_image_id_id_apply, atac])
         (1 upto (m + n) ~~ set_map0s)];
@@ -290,7 +279,7 @@
     CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
       EVERY' [rtac allI, rtac allI, rtac impI,
         rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-        REPEAT_DETERM_N m o rtac conversep_in_rel_Id_on,
+        REPEAT_DETERM_N m o rtac @{thm conversep_eq},
         REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
         rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
         REPEAT_DETERM o etac allE,
@@ -303,7 +292,7 @@
     CONJ_WRAP' (fn (rel_cong, rel_OO) =>
       EVERY' [rtac allI, rtac allI, rtac impI,
         rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-        REPEAT_DETERM_N m o rtac relcompp_in_rel_Id_on,
+        REPEAT_DETERM_N m o rtac @{thm eq_OO},
         REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
         rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
         etac @{thm relcompE},
@@ -313,7 +302,7 @@
         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
 
 fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
-  unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
+  unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
     CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -373,13 +362,11 @@
   let
     val n = length strT_defs;
     val ks = 1 upto n;
-    fun coalg_tac (i, ((passive_sets, active_sets), def)) =
+    fun coalg_tac (i, (active_sets, def)) =
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
         hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
         rtac (mk_sum_caseN n i), rtac CollectI,
-        EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
-          etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
-          passive_sets),
+        REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
         CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
           rtac conjI,
@@ -397,7 +384,6 @@
               REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
               rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
               rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
-              REPEAT_DETERM_N m o (rtac conjI THEN' atac),
               CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
                 rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
                 rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
@@ -414,7 +400,7 @@
             rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
   in
     unfold_thms_tac ctxt defs THEN
-    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_map0ss ~~ strT_defs)) 1
+    CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1
   end;
 
 fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
@@ -519,35 +505,6 @@
       ks)] 1
   end;
 
-fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
-  let
-    val n = length Lev_0s;
-    val ks = 1 upto n;
-  in
-    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
-        EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
-          dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
-          rtac (rv_Nil RS arg_cong RS iffD2),
-          rtac (mk_sum_caseN n i RS iffD2),
-          CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
-      (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
-        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
-          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
-            (fn (i, (from_to_sbd, coalg_set)) =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
-              rtac (rv_Cons RS arg_cong RS iffD2),
-              rtac (mk_sum_caseN n i RS arg_cong RS trans RS iffD2),
-              etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
-              dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
-              etac coalg_set, atac])
-          (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
-      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
-  end;
-
 fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
   let
     val n = length Lev_0s;
@@ -655,7 +612,7 @@
 
 fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
-  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
+  prefCl_Levs rv_lastss set_Levsss set_image_Levsss set_map0ss
   map_comp_ids map_cong0s map_arg_congs =
   let
     val n = length beh_defs;
@@ -663,7 +620,7 @@
 
     fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
       ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s,
-        (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
+        (set_Levss, set_image_Levss))))))))))) =
       EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
         rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
         rtac conjI,
@@ -678,18 +635,12 @@
         rtac conjI,
           rtac ballI, etac @{thm UN_E}, rtac conjI,
           if n = 1 then K all_tac else rtac (mk_sumEN n),
-          EVERY' (map6 (fn i => fn isNode_def => fn set_map0s =>
-            fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
+          EVERY' (map5 (fn i => fn isNode_def => fn set_map0s => fn set_Levs => fn set_image_Levs =>
             EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
               rtac exI, rtac conjI,
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
                 etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
-              EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
-                  rtac trans_fun_cong_image_id_id_apply,
-                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
-              (take m set_map0s) set_rv_Levs),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                 EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -699,9 +650,9 @@
                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                   if n = 1 then rtac refl else atac])
               (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
-          ks isNode_defs set_map0ss set_rv_Levss set_Levss set_image_Levss),
+          ks isNode_defs set_map0ss set_Levss set_image_Levss),
           CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
-            (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
+            (set_Levs, set_image_Levs))))) =>
             EVERY' [rtac ballI,
               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
               rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
@@ -709,11 +660,6 @@
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
                 etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
-              EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
-                  rtac trans_fun_cong_image_id_id_apply,
-                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
-              (take m set_map0s) set_rv_Levs),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                 EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -726,7 +672,7 @@
                   if n = 1 then rtac refl else atac])
               (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
           (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
-            (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
+            (set_Levss ~~ set_image_Levss))))),
         (**)
           rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
           etac notE, etac @{thm UN_I[OF UNIV_I]},
@@ -736,10 +682,6 @@
           CONVERSION (Conv.top_conv
             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
           if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
-          EVERY' (map2 (fn set_map0 => fn coalg_set =>
-            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
-              rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
-            (take m set_map0s) (take m coalg_sets)),
           CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
             EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
               rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
@@ -768,7 +710,7 @@
         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
           DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
-            rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
+            rtac equalityI, rtac subsetI, etac thin_rl, 
             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
             etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
@@ -811,8 +753,7 @@
     CONJ_WRAP' fbetw_tac
       (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
         ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
-          (set_map0ss ~~ (coalg_setss ~~
-            (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
+          (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))))) THEN'
     CONJ_WRAP' mor_tac
       (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
         ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
@@ -834,16 +775,12 @@
     CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
       EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
         rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
-        EVERY' (map2 (fn set_map0 => fn coalgT_set =>
-          EVERY' [rtac conjI, rtac (set_map0 RS ord_eq_le_trans),
-            rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
-            etac coalgT_set])
-        (take m set_map0s) (take m coalgT_sets)),
+        REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
         CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
           EVERY' [rtac (set_map0 RS ord_eq_le_trans),
             rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
             rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
-        (equiv_LSBISs ~~ drop m (set_map0s ~~ coalgT_sets))])
+        (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))])
     ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
 
 fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
@@ -856,7 +793,7 @@
         rtac congruent_str_final, atac, rtac o_apply])
     (equiv_LSBISs ~~ congruent_str_finals)] 1;
 
-fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
+fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
   unfold_thms_tac ctxt defs THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
@@ -865,7 +802,7 @@
         EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
           EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
             etac set_rev_mp, rtac coalg_final_set, rtac Rep])
-        Abs_inverses (drop m coalg_final_sets))])
+        Abs_inverses coalg_final_sets)])
     (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
 
 fun mk_mor_Abs_tac ctxt defs Abs_inverses =
@@ -940,7 +877,7 @@
     rel_congs,
     CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
       REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-      REPEAT_DETERM_N m o rtac @{thm in_rel_Id_on_UNIV[symmetric]},
+      REPEAT_DETERM_N m o rtac refl,
       REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
       etac mp, etac CollectE, etac @{thm splitD}])
     rel_congs,
diff -r 892a425c5eaa -r fd9ea8ae28f6 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Feb 18 14:51:26 2014 +0100
@@ -85,7 +85,6 @@
     val FTsAs = mk_FTs allAs;
     val FTsBs = mk_FTs allBs;
     val FTsCs = mk_FTs allCs;
-    val ATs = map HOLogic.mk_setT passiveAs;
     val BTs = map HOLogic.mk_setT activeAs;
     val B'Ts = map HOLogic.mk_setT activeBs;
     val B''Ts = map HOLogic.mk_setT activeCs;
@@ -120,11 +119,10 @@
       bd0s Dss bnfs;
     val witss = map wits_of_bnf bnfs;
 
-    val (((((((((((((((((((zs, zs'), As), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
+    val ((((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
       fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), (yFs, yFs')),
       names_lthy) = lthy
       |> mk_Frees' "z" activeAs
-      ||>> mk_Frees "A" ATs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B'" B'Ts
@@ -245,16 +243,16 @@
     val alg_bind = mk_internal_b algN;
     val alg_def_bind = (Thm.def_binding alg_bind, []);
 
-    (*forall i = 1 ... n: (\<forall>x \<in> Fi_in A1 .. Am B1 ... Bn. si x \<in> Bi)*)
+    (*forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> Bi)*)
     val alg_spec =
       let
-        val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
+        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
         fun mk_alg_conjunct B s X x x' =
           mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
 
         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
+        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
       end;
 
     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
@@ -264,11 +262,11 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
-    val alg_def = mk_unabs_def (live + n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
+    val alg_def = mk_unabs_def (2 * n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
 
-    fun mk_alg As Bs ss =
+    fun mk_alg Bs ss =
       let
-        val args = As @ Bs @ ss;
+        val args = Bs @ ss;
         val Ts = map fastype_of args;
         val algT = Library.foldr (op -->) (Ts, HOLogic.boolT);
       in
@@ -277,13 +275,13 @@
 
     val alg_set_thms =
       let
-        val alg_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
         fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
-        val premss = map2 ((fn x => fn sets =>  map2 (mk_prem x) sets (As @ Bs))) xFs setssAs;
+        val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
         val concls = map3 mk_concl ss xFs Bs;
         val goals = map3 (fn x => fn prems => fn concl =>
-          fold_rev Logic.all (x :: As @ Bs @ ss)
+          fold_rev Logic.all (x :: Bs @ ss)
             (Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
       in
         map (fn goal =>
@@ -291,12 +289,12 @@
         goals
       end;
 
-    fun mk_talg ATs BTs = mk_alg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
+    fun mk_talg BTs = mk_alg (map HOLogic.mk_UNIV BTs);
 
     val talg_thm =
       let
         val goal = fold_rev Logic.all ss
-          (HOLogic.mk_Trueprop (mk_talg passiveAs activeAs ss))
+          (HOLogic.mk_Trueprop (mk_talg activeAs ss))
       in
         Goal.prove_sorry lthy [] [] goal
           (K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
@@ -308,7 +306,7 @@
     val alg_not_empty_thms =
       let
         val alg_prem =
-          HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+          HOLogic.mk_Trueprop (mk_alg Bs ss);
         val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
         val goals =
           map (fn concl =>
@@ -415,9 +413,7 @@
         fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
           HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
         val prems = map HOLogic.mk_Trueprop
-          ([mk_mor Bs ss B's s's fs,
-          mk_alg passive_UNIVs Bs ss,
-          mk_alg passive_UNIVs B's s's] @
+          ([mk_mor Bs ss B's s's fs, mk_alg Bs ss, mk_alg B's s's] @
           map4 mk_inv_prem fs inv_fs Bs B's);
         val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
       in
@@ -497,9 +493,7 @@
 
     val iso_alt_thm =
       let
-        val prems = map HOLogic.mk_Trueprop
-         [mk_alg passive_UNIVs Bs ss,
-         mk_alg passive_UNIVs B's s's]
+        val prems = map HOLogic.mk_Trueprop [mk_alg Bs ss, mk_alg B's s's]
         val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
           HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
             Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
@@ -517,7 +511,7 @@
     val (copy_alg_thm, ex_copy_alg_thm) =
       let
         val prems = map HOLogic.mk_Trueprop
-         (mk_alg passive_UNIVs Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
+         (mk_alg Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
         val inver_prems = map HOLogic.mk_Trueprop
           (map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's);
         val all_prems = prems @ inver_prems;
@@ -525,7 +519,7 @@
           (Term.list_comb (mapT, passive_ids @ inv_fs) $ y)));
 
         val alg = HOLogic.mk_Trueprop
-          (mk_alg passive_UNIVs B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
+          (mk_alg B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
         val copy_str_thm = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
             (Logic.list_implies (all_prems, alg)))
@@ -542,7 +536,7 @@
 
         val ex = HOLogic.mk_Trueprop
           (list_exists_free s's
-            (HOLogic.mk_conj (mk_alg passive_UNIVs B's s's,
+            (HOLogic.mk_conj (mk_alg B's s's,
               mk_iso B's s's Bs ss inv_fs fs_copy)));
         val ex_copy_alg_thm = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
@@ -593,7 +587,9 @@
     val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
       [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
 
-    val Asuc_bdT = fst (dest_relT (fastype_of (mk_Asuc_bd As)));
+
+    val Asuc_bd = mk_Asuc_bd passive_UNIVs;
+    val Asuc_bdT = fst (dest_relT (fastype_of Asuc_bd));
     val II_BTs = replicate n (HOLogic.mk_setT Asuc_bdT);
     val II_sTs = map2 (fn Ds => fn bnf =>
       mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs;
@@ -631,31 +627,31 @@
     fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i)
       (Term.absfree jdx' (mk_nthN n (Asi $ jdx) k));
 
-    fun mk_minH_component As Asi i sets Ts s k =
+    fun mk_minH_component Asi i sets Ts s k =
       HOLogic.mk_binop @{const_name "sup"}
-      (mk_minG Asi i k, mk_image s $ mk_in (As @ map (mk_minG Asi i) ks) sets Ts);
+      (mk_minG Asi i k, mk_image s $ mk_in (passive_UNIVs @ map (mk_minG Asi i) ks) sets Ts);
 
-    fun mk_min_algs As ss =
+    fun mk_min_algs ss =
       let
         val BTs = map (range_type o fastype_of) ss;
-        val Ts = map (HOLogic.dest_setT o fastype_of) As @ BTs;
+        val Ts = passiveAs @ BTs;
         val (Asi, Asi') = `Free (Asi_name, suc_bdT -->
           Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
       in
          mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
-           (map4 (mk_minH_component As Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
+           (map4 (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
       end;
 
     val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
       let
         val i_field = HOLogic.mk_mem (idx, field_suc_bd);
-        val min_algs = mk_min_algs As ss;
+        val min_algs = mk_min_algs ss;
         val min_algss = map (fn k => mk_nthN n (min_algs $ idx) k) ks;
 
         val concl = HOLogic.mk_Trueprop
           (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
-            (map4 (mk_minH_component As min_algs idx) setssAs FTsAs ss ks)));
-        val goal = fold_rev Logic.all (idx :: As @ ss)
+            (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
+        val goal = fold_rev Logic.all (idx :: ss)
           (Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
 
         val min_algs_thm = Goal.prove_sorry lthy [] [] goal
@@ -665,7 +661,7 @@
         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
 
         fun mk_mono_goal min_alg =
-          fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_relChain suc_bd
+          fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_relChain suc_bd
             (Term.absfree idx' min_alg)));
 
         val monos =
@@ -674,8 +670,6 @@
             |> Thm.close_derivation)
           (map mk_mono_goal min_algss) min_algs_thms;
 
-        val Asuc_bd = mk_Asuc_bd As;
-
         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
         val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
         val card_cT = certifyT lthy suc_bdT;
@@ -690,7 +684,7 @@
               suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
           |> Thm.close_derivation;
 
-        val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+        val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
         val least_cT = certifyT lthy suc_bdT;
         val least_ct = certify lthy (Term.absfree idx' least_conjunction);
@@ -715,9 +709,9 @@
     fun min_alg_spec i =
       let
         val rhs = mk_UNION (field_suc_bd)
-          (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
+          (Term.absfree idx' (mk_nthN n (mk_min_algs ss $ idx) i));
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ ss) rhs
+        fold_rev (Term.absfree o Term.dest_Free) ss rhs
       end;
 
     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
@@ -730,47 +724,45 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
     val min_alg_defs = map (fn def =>
-      mk_unabs_def live (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
+      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
 
-    fun mk_min_alg As ss i =
+    fun mk_min_alg ss i =
       let
         val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1))))
-        val args = As @ ss;
-        val Ts = map fastype_of args;
+        val Ts = map fastype_of ss;
         val min_algT = Library.foldr (op -->) (Ts, T);
       in
-        Term.list_comb (Const (nth min_algs (i - 1), min_algT), args)
+        Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss)
       end;
 
     val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
       let
-        val min_algs = map (mk_min_alg As ss) ks;
+        val min_algs = map (mk_min_alg ss) ks;
 
-        val goal = fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_alg As min_algs ss));
+        val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
         val alg_min_alg = Goal.prove_sorry lthy [] [] goal
           (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
             set_bd_sumss min_algs_thms min_algs_mono_thms))
           |> Thm.close_derivation;
 
-        val Asuc_bd = mk_Asuc_bd As;
         fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ ss)
+          (fold_rev Logic.all ss
             (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
           (K (mk_card_of_min_alg_tac def card_of_min_algs_thm
             suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
           |> Thm.close_derivation;
 
-        val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+        val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss)
+          (fold_rev Logic.all (Bs @ ss)
             (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
           (K (mk_least_min_alg_tac def least_min_algs_thm))
           |> Thm.close_derivation;
 
         val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
 
-        val incl_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
-        val incl_min_algs = map (mk_min_alg passive_UNIVs ss) ks;
+        val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
+        val incl_min_algs = map (mk_min_alg ss) ks;
         val incl = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss)
             (Logic.mk_implies (incl_prem,
@@ -812,7 +804,7 @@
     val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
       (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
         Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))),
-        mk_alg passive_UNIVs II_Bs II_ss)));
+        mk_alg II_Bs II_ss)));
 
     val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
     val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
@@ -849,23 +841,23 @@
     val str_init_defs = map (fn def =>
       mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
 
-    val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks;
+    val car_inits = map (mk_min_alg str_inits) ks;
 
     (*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
     val alg_init_thm = Goal.prove_sorry lthy [] []
-      (HOLogic.mk_Trueprop (mk_alg passive_UNIVs car_inits str_inits))
+      (HOLogic.mk_Trueprop (mk_alg car_inits str_inits))
       (K (rtac alg_min_alg_thm 1))
       |> Thm.close_derivation;
 
     val alg_select_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_Ball II
-        (Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
+        (Term.absfree iidx' (mk_alg select_Bs select_ss))))
       (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
       |> Thm.close_derivation;
 
     val mor_select_thm =
       let
-        val alg_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
         val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss Bs ss Asuc_fs);
         val prems = [alg_prem, i_prem, mor_prem];
@@ -882,7 +874,7 @@
 
     val (init_ex_mor_thm, init_unique_mor_thms) =
       let
-        val prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+        val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val concl = HOLogic.mk_Trueprop
           (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
         val ex_mor = Goal.prove_sorry lthy [] []
diff -r 892a425c5eaa -r fd9ea8ae28f6 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 18 01:11:25 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 18 14:51:26 2014 +0100
@@ -89,16 +89,13 @@
 val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
 
 fun mk_alg_set_tac alg_def =
-  dtac (alg_def RS iffD1) 1 THEN
-  REPEAT_DETERM (etac conjE 1) THEN
-  EVERY' [etac bspec, rtac CollectI] 1 THEN
-  REPEAT_DETERM (etac conjI 1) THEN atac 1;
+  EVERY' [dtac (alg_def RS iffD1), REPEAT_DETERM o etac conjE, etac bspec, rtac CollectI,
+   REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
 
 fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
   (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
   REPEAT_DETERM o FIRST'
-    [rtac subset_UNIV,
-    EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
+    [EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
     EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
     EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt,
       FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
@@ -220,7 +217,7 @@
       CONJ_WRAP' (fn (thms, thm) =>
         EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
           rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm,
-          REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
+          REPEAT_DETERM_N n o set_tac thms])
       (set_maps ~~ alg_sets);
   in
     (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
@@ -238,7 +235,7 @@
     val mor_tac =
       CONJ_WRAP' (fn (thms, thm) =>
         EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm,
-          REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
+          REPEAT_DETERM_N n o set_tac thms])
       (set_maps ~~ alg_sets);
   in
     (rtac (iso_alt RS iffD2) THEN'
@@ -340,7 +337,7 @@
     fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ord_eq_le_trans, etac min_alg,
       rtac @{thm Un_least}, minG_tac, rtac @{thm image_subsetI},
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac alg_set,
-      REPEAT_DETERM o FIRST' [atac, etac subset_trans THEN' minG_tac]];
+      REPEAT_DETERM o (etac subset_trans THEN' minG_tac)];
   in
     (rtac induct THEN'
     rtac impI THEN'
@@ -397,9 +394,8 @@
     fun alg_epi_tac ((alg_set, str_init_def), set_map) =
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
         rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set,
-        REPEAT_DETERM o FIRST' [rtac subset_UNIV,
-          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]]];
+        REPEAT_DETERM o 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 comp_id}) THEN'
     rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
@@ -448,7 +444,6 @@
 
     fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
-      REPEAT_DETERM_N m o rtac subset_UNIV,
       REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
       rtac trans, mor_tac morE in_mono,
       rtac trans, cong_tac map_cong0,
@@ -468,7 +463,6 @@
 
     fun mk_alg_tac alg_set = EVERY' [rtac ballI, rtac CollectI,
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
-      REPEAT_DETERM_N m o rtac subset_UNIV,
       REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
       rtac mp, etac bspec, rtac CollectI,
       REPEAT_DETERM_N m o (rtac conjI THEN' atac),