# HG changeset patch
# User blanchet
# Date 1347424235 -7200
# Node ID 3f8671b353aea89518a0e09cfd41b1f6775b910a
# Parent  c874ff5658dc9d429b343da59c997faf2fdd88d0
tuning

diff -r c874ff5658dc -r 3f8671b353ae src/HOL/Codatatype/BNF_GFP.thy
--- a/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 06:27:48 2012 +0200
+++ b/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 06:30:35 2012 +0200
@@ -8,7 +8,7 @@
 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_GFP
-imports BNF_FP
+imports BNF_FP Equiv_Relations_More
 keywords
   "codata_raw" :: thy_decl and
   "codata" :: thy_decl
diff -r c874ff5658dc -r 3f8671b353ae src/HOL/Codatatype/BNF_Util.thy
--- a/src/HOL/Codatatype/BNF_Util.thy	Wed Sep 12 06:27:48 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Util.thy	Wed Sep 12 06:30:35 2012 +0200
@@ -12,7 +12,6 @@
 imports
   "../Cardinals/Cardinal_Arithmetic"
   "~~/src/HOL/Library/Prefix_Order"
-  Equiv_Relations_More
 begin
 
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
diff -r c874ff5658dc -r 3f8671b353ae src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 06:27:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 06:30:35 2012 +0200
@@ -1390,7 +1390,7 @@
         val p1s_maps = map (mk_map XTs p1s Ts flds (mk_passive_maps passiveXs passiveAs)) ks;
         val p2s_maps = map (mk_map XTs p2s Ts' fld's (mk_passive_maps passiveXs passiveBs)) ks;
 
-        val (map_simp_thms, map_thms) =
+        val map_simp_thms =
           let
             fun mk_goal fs_map map fld fld' = fold_rev Logic.all fs
               (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, fld),
@@ -1402,7 +1402,7 @@
                 |> Thm.close_derivation)
               goals iter_thms map_comp_id_thms map_congs;
           in
-            map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
+            map (fn thm => thm RS @{thm pointfreeE}) maps
           end;
 
         val (map_unique_thms, map_unique_thm) =
@@ -1450,7 +1450,7 @@
         val setss_by_range = map (fn cols => map (mk_iter Ts cols) ks) colss;
         val setss_by_bnf = transpose setss_by_range;
 
-        val (set_simp_thmss, set_thmss) =
+        val set_simp_thmss =
           let
             fun mk_goal sets fld set col map =
               mk_Trueprop_eq (HOLogic.mk_comp (set, fld),
@@ -1477,7 +1477,7 @@
                 |> Thm.close_derivation)
               set_natural'ss) ls simp_goalss setss;
           in
-            (set_simpss, setss)
+            set_simpss
           end;
 
         fun mk_set_thms set_simp = (@{thm xt1(3)} OF [set_simp, @{thm Un_upper1}]) ::