# HG changeset patch
# User traytel
# Date 1380719621 -7200
# Node ID 4d087a8950f39692420854d21bb04622e2f59395
# Parent  e5853a648b59b1855d02b13c130d3065fcd77bb5
made SML/NJ happy

diff -r e5853a648b59 -r 4d087a8950f3 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 13:29:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 15:13:41 2013 +0200
@@ -394,7 +394,7 @@
 
 local
 
-fun gen_primrec prep_spec raw_fixes raw_spec lthy =
+fun gen_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
   let
     val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
     val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d);