# HG changeset patch
# User blanchet
# Date 1346786591 -7200
# Node ID 81487fc171850fd20dbb5d5b62cfdad3606f3d1e
# Parent  3c26e17b2849d46d67927bfb92ad170ef70c5b9b
added robustness

diff -r 3c26e17b2849 -r 81487fc17185 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 18:49:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 04 21:23:11 2012 +0200
@@ -255,10 +255,8 @@
 fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
   (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
 
-fun mk_fp_bnf timer construct bs sort bnfs deads lives unfold lthy =
+fun mk_fp_bnf timer construct bs sort bnfs deadss livess unfold lthy =
   let
-    (* TODO: assert that none of the deads is a lhs *)
-
     val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
     fun qualify i bind =
       let val namei = if i > 0 then name ^ string_of_int i else name;
@@ -267,15 +265,19 @@
         else Binding.prefix_name namei bind
       end;
 
-    val Ass = map (map dest_TFree) lives;
-    val Ds = fold (fold Term.add_tfreesT) deads [];
+    val Ass = map (map dest_TFree) livess;
+    val Ds = fold (fold Term.add_tfreesT) deadss [];
+
+    val _ = (case Library.inter (op =) Ds (fold (union (op =)) Ass []) of [] => ()
+      | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
+        \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
 
     val timer = time (timer "Construction of BNFs");
 
     val ((kill_poss, _), (bnfs', (unfold', lthy'))) =
       normalize_bnfs qualify Ass Ds sort bnfs unfold lthy;
 
-    val Dss = map3 (append oo map o nth) lives kill_poss deads;
+    val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
     val (bnfs'', lthy'') =
       fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy';
diff -r 3c26e17b2849 -r 81487fc17185 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 18:49:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 21:23:11 2012 +0200
@@ -26,10 +26,10 @@
 fun bnf_lfp bs Dss_insts bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
-    val live = live_of_bnf (hd bnfs)
+    val live = live_of_bnf (hd bnfs);
     val n = length bnfs; (*active*)
-    val ks = 1 upto n
-    val m = live - n (*passive, if 0 don't generate a new bnf*)
+    val ks = 1 upto n;
+    val m = live - n; (*passive, if 0 don't generate a new bnf*)
     val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
 
     (* TODO: check if m, n etc are sane *)