1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 11 10:23:01 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 11 16:41:08 2013 +0100
     1.3 @@ -99,10 +99,6 @@
     1.4      val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
     1.5      val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
     1.6  
     1.7 -    fun abstract t =
     1.8 -      let val Ts = Term.add_frees t [];
     1.9 -      in fold_rev Term.absfree (filter (member op = Ts) phis') t end;
    1.10 -
    1.11      val rels =
    1.12        let
    1.13          fun find_rel T As Bs = fp_nesty_bnfss
    1.14 @@ -125,7 +121,7 @@
    1.15                handle General.Subscript => HOLogic.eq_const T)
    1.16            | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
    1.17        in
    1.18 -        map2 (abstract oo mk_rel) fpTs fpTs'
    1.19 +        map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
    1.20        end;
    1.21  
    1.22      val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;