# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 2e91e9bbc2123be16c60a0e814d338e91794dc9b
# Parent  16648edf16e3a4767edcea290dfb8cde40f7155d
made SML/NJ happier

diff -r 16648edf16e3 -r 2e91e9bbc212 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -288,7 +288,7 @@
       else
         ((fp_sugars, (NONE, NONE)), lthy);
 
-    fun mk_ctr_of {ctr_sugar = {ctrs, ...}, ...} (Type (_, Ts)) = map (mk_ctr Ts) ctrs;
+    fun mk_ctr_of ({ctr_sugar = {ctrs, ...}, ...} : fp_sugar) (Type (_, Ts)) = map (mk_ctr Ts) ctrs;
     val substAT = Term.typ_subst_atomic (var_As ~~ As);
 
     val Xs' = map #X fp_sugars';