src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
changeset 59314 91649ea1b32c
parent 59281 1b4dc8a9f7d9
child 59595 2d90b85b9264
--- 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,