# HG changeset patch
# User wenzelm
# Date 1428703087 -7200
# Node ID 41a11782509771b8712e91327858aa8be942530d
# Parent  fd9191f0d32338a721d9bbbbfde1ba017abeee18
make SML/NJ more happy;

diff -r fd9191f0d323 -r 41a117825097 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Apr 10 23:56:41 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Apr 10 23:58:07 2015 +0200
@@ -617,7 +617,7 @@
 
 fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy =
   let
-    val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
+    val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes);
     val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
 
     val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)