Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made SML/NJ happier
authorblanchet
Tue, 02 Sep 2014 12:11:04 +0200
changeset 58137 feb69891e0fd
parent 58136 10f92532f128
child 58138 3bfd12e456f4
made SML/NJ happier
src/HOL/Tools/BNF/bnf_lfp_compat.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle