# HG changeset patch
# User traytel
# Date 1384184468 -3600
# Node ID 347c3b0cab444525f23c4a3c189e9b2d2c27d7ad
# Parent  3fc1b77ef750121df8c9138bf49d493df15e9cac
handle independent functions defined in parallel in N2M (in presence of type variables, see ce58fb149ff6)

diff -r 3fc1b77ef750 -r 347c3b0cab44 src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 11 10:23:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML	Mon Nov 11 16:41:08 2013 +0100
@@ -99,10 +99,6 @@
     val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
     val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
 
-    fun abstract t =
-      let val Ts = Term.add_frees t [];
-      in fold_rev Term.absfree (filter (member op = Ts) phis') t end;
-
     val rels =
       let
         fun find_rel T As Bs = fp_nesty_bnfss
@@ -125,7 +121,7 @@
               handle General.Subscript => HOLogic.eq_const T)
           | mk_rel _ _ = raise Fail "fpTs contains schematic type variables";
       in
-        map2 (abstract oo mk_rel) fpTs fpTs'
+        map2 (fold_rev Term.absfree phis' oo mk_rel) fpTs fpTs'
       end;
 
     val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;