1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 10:11:14 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 10:16:40 2013 +0200
     1.3 @@ -385,14 +385,6 @@
     1.4          | _ => build_simple TU);
     1.5    in build end;
     1.6  
     1.7 -fun build_rel_step lthy build_arg (Type (s, Ts)) =
     1.8 -  let
     1.9 -    val bnf = the (bnf_of lthy s);
    1.10 -    val live = live_of_bnf bnf;
    1.11 -    val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
    1.12 -    val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
    1.13 -  in Term.list_comb (rel, map build_arg Ts') end;
    1.14 -
    1.15  fun derive_induct_fold_rec_thms_for_types pre_bnfs ctor_folds0 ctor_recs0 ctor_induct ctor_fold_thms
    1.16      ctor_rec_thms nesting_bnfs nested_bnfs fpTs Cs As ctrss ctr_defss folds recs fold_defs rec_defs
    1.17      lthy =
    1.18 @@ -607,12 +599,19 @@
    1.19          fun build_rel rs' T =
    1.20            (case find_index (curry (op =) T) fpTs of
    1.21              ~1 =>
    1.22 -            if exists_subtype_in fpTs T then build_rel_step lthy (build_rel rs') T
    1.23 -            else HOLogic.eq_const T
    1.24 +            if exists_subtype_in fpTs T then
    1.25 +              let
    1.26 +                val Type (s, Ts) = T
    1.27 +                val bnf = the (bnf_of lthy s);
    1.28 +                val live = live_of_bnf bnf;
    1.29 +                val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
    1.30 +                val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
    1.31 +              in Term.list_comb (rel, map (build_rel rs') Ts') end
    1.32 +            else
    1.33 +              HOLogic.eq_const T
    1.34            | kk => nth rs' kk);
    1.35  
    1.36 -        fun build_rel_app rs' usel vsel =
    1.37 -          fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
    1.38 +        fun build_rel_app rs' usel vsel = fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
    1.39  
    1.40          fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
    1.41            (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @