# HG changeset patch
# User blanchet
# Date 1385124120 -3600
# Node ID d71c2737ee2149e5ee251aa521a835cb83219ebd
# Parent  dd511ddcb203d00c05490a76863e2eca59c31874
correctly account for dead variables when naming set functions

diff -r dd511ddcb203 -r d71c2737ee21 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Nov 22 13:42:00 2013 +0100
@@ -56,7 +56,7 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all BNFs have the same lives*)
-fun construct_gfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes map_bs rel_bs set_bss0 bs resBs (resDs, Dss) bnfs lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
@@ -2673,6 +2673,10 @@
 
         val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
+        val set_bss =
+          map (flat o map2 (fn B => fn b =>
+            if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
+
         val (Jbnfs, lthy) =
           fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
               fn T => fn (thms, wits) => fn lthy =>
diff -r dd511ddcb203 -r d71c2737ee21 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Nov 22 13:42:00 2013 +0100
@@ -27,7 +27,7 @@
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes map_bs rel_bs set_bss0 bs resBs (resDs, Dss) bnfs lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
@@ -1744,6 +1744,10 @@
         fun wit_tac {context = ctxt, prems = _} =
           mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
+        val set_bss =
+          map (flat o map2 (fn B => fn b =>
+            if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
+
         val (Ibnfs, lthy) =
           fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
               fn T => fn wits => fn lthy =>
diff -r dd511ddcb203 -r d71c2737ee21 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Nov 22 13:42:00 2013 +0100
@@ -11,7 +11,7 @@
 subsection "Infinite Sets"
 
 text {*
-  Some elementary facts about infinite sets, mostly by Stefan Merz.
+  Some elementary facts about infinite sets, mostly by Stephan Merz.
   Beware! Because "infinite" merely abbreviates a negation, these
   lemmas may not work well with @{text "blast"}.
 *}