# HG changeset patch
# User traytel
# Date 1346851357 -7200
# Node ID 2a361e09101bf4ca2c0051fe2cfadb77b7f966e0
# Parent  f51ab68f882fcb8c4795f9419d1b2034a40bcf11
error message only in case of an error

diff -r f51ab68f882f -r 2a361e09101b src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 14:49:35 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 15:22:37 2012 +0200
@@ -259,7 +259,7 @@
 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 resBs sort bnfs deadss livess unfold lthy =
+fun mk_fp_bnf timer construct bs resBs sort lhss bnfs deadss livess unfold lthy =
   let
     val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
     fun qualify i bind =
@@ -273,7 +273,7 @@
     val resDs = fold (subtract (op =)) Ass resBs;
     val Ds = fold (fold Term.add_tfreesT) deadss resDs;
 
-    val _ = (case Library.inter (op =) Ds (fold (union (op =)) Ass []) of [] => ()
+    val _ = (case Library.inter (op =) Ds lhss of [] => ()
       | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
         \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
 
@@ -305,7 +305,7 @@
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
         (empty_unfold, lthy));
   in
-    mk_fp_bnf timer construct bs resBs sort bnfs Dss Ass unfold lthy'
+    mk_fp_bnf timer construct bs resBs sort lhss bnfs Dss Ass unfold lthy'
   end;
 
 fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
@@ -318,7 +318,7 @@
         (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
         bs raw_bnfs (empty_unfold, lthy));
   in
-    mk_fp_bnf timer construct bs [] sort bnfs Dss Ass unfold lthy'
+    mk_fp_bnf timer construct bs [] sort lhss bnfs Dss Ass unfold lthy'
   end;
 
 end;