src/HOL/BNF/Tools/bnf_fp_n2m.ML

     val pre_bnfss = map #pre_bnfs fp_sugars;
     val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
     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
           |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
           |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))

               end
           | mk_rel (T as TFree _) _ = (nth phis (find_index (curry op = T) As)
               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;
 
     val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;