# HG changeset patch
# User blanchet
# Date 1409652664 -7200
# Node ID feb69891e0fdabfb6c1ae9f128945303a407991c
# Parent  10f92532f128b0e01d765613d564a00232cfb24c
made SML/NJ happier

diff -r 10f92532f128 -r feb69891e0fd src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Sep 02 12:09:13 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Sep 02 12:11:04 2014 +0200
@@ -263,7 +263,7 @@
   else
     thy;
 
-fun new_interpretation_of nesting_pref f fp_sugars thy =
+fun new_interpretation_of nesting_pref f (fp_sugars : fp_sugar list) thy =
   let val T_names = map (fst o dest_Type o #T) fp_sugars in
     if nesting_pref = Keep_Nesting orelse
         exists (is_none o Old_Datatype_Data.get_info thy) T_names then