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;