# HG changeset patch
# User blanchet
# Date 1420617980 -3600
# Node ID 91649ea1b32ca0c909d74d409edacc646d161e92
# Parent  d7f4f46e9a591b40a2da30c66cbaa4ddb5c20bfc
made SML/NJ happier

diff -r d7f4f46e9a59 -r 91649ea1b32c src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Jan 07 00:10:23 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Jan 07 09:06:20 2015 +0100
@@ -69,7 +69,7 @@
    fun_defs: thm list,
    fpTs: typ list};
 
-fun morph_fp_rec_sugar phi {transfers, fun_names, funs, fun_defs, fpTs} =
+fun morph_fp_rec_sugar phi ({transfers, fun_names, funs, fun_defs, fpTs} : fp_rec_sugar) =
   {transfers = transfers,
    fun_names = fun_names,
    funs = map (Morphism.term phi) funs,