# 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)