# HG changeset patch
# User traytel
# Date 1393702831 -3600
# Node ID e21d83c8e1c74719dc6799d10b275612c9f7a5b8
# Parent  d8b2f50705d00bfd355e401d07e79f0f599b7a5f
made SML/NJ happier

diff -r d8b2f50705d0 -r e21d83c8e1c7 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Sat Mar 01 17:08:39 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Sat Mar 01 20:40:31 2014 +0100
@@ -47,7 +47,7 @@
   end;
 
 fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
-    absT_infos lthy =
+    (absT_infos : absT_info list) lthy =
   let
     fun of_fp_res get =
       map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
@@ -122,13 +122,10 @@
     val xTs = map (domain_type o fastype_of) xtors;
     val yTs = map (domain_type o fastype_of) xtor's;
 
-    fun abs_of allAs Ds bnf = mk_abs (mk_T_of_bnf Ds allAs bnf) o #abs;
-    fun rep_of absAT = mk_rep absAT o #rep;
-
-    val absAs = map3 (abs_of allAs) Dss bnfs absT_infos;
-    val absBs = map3 (abs_of allBs) Dss bnfs absT_infos;
-    val fp_repAs = map2 rep_of absATs fp_absT_infos;
-    val fp_repBs = map2 rep_of absBTs fp_absT_infos;
+    val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
+    val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
+    val fp_repAs = map2 mk_rep absATs fp_reps;
+    val fp_repBs = map2 mk_rep absBTs fp_reps;
 
     val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
       |> mk_Frees' "R" phiTs