1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 14:49:35 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 15:22:37 2012 +0200
     1.3 @@ -259,7 +259,7 @@
     1.4  fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
     1.5    (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
     1.6  
     1.7 -fun mk_fp_bnf timer construct bs resBs sort bnfs deadss livess unfold lthy =
     1.8 +fun mk_fp_bnf timer construct bs resBs sort lhss bnfs deadss livess unfold lthy =
     1.9    let
    1.10      val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
    1.11      fun qualify i bind =
    1.12 @@ -273,7 +273,7 @@
    1.13      val resDs = fold (subtract (op =)) Ass resBs;
    1.14      val Ds = fold (fold Term.add_tfreesT) deadss resDs;
    1.15  
    1.16 -    val _ = (case Library.inter (op =) Ds (fold (union (op =)) Ass []) of [] => ()
    1.17 +    val _ = (case Library.inter (op =) Ds lhss of [] => ()
    1.18        | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
    1.19          \variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
    1.20  
    1.21 @@ -305,7 +305,7 @@
    1.22        (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
    1.23          (empty_unfold, lthy));
    1.24    in
    1.25 -    mk_fp_bnf timer construct bs resBs sort bnfs Dss Ass unfold lthy'
    1.26 +    mk_fp_bnf timer construct bs resBs sort lhss bnfs Dss Ass unfold lthy'
    1.27    end;
    1.28  
    1.29  fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
    1.30 @@ -318,7 +318,7 @@
    1.31          (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
    1.32          bs raw_bnfs (empty_unfold, lthy));
    1.33    in
    1.34 -    mk_fp_bnf timer construct bs [] sort bnfs Dss Ass unfold lthy'
    1.35 +    mk_fp_bnf timer construct bs [] sort lhss bnfs Dss Ass unfold lthy'
    1.36    end;
    1.37  
    1.38  end;