make SML/NJ more happy;
authorwenzelm
Fri Apr 10 23:58:07 2015 +0200 (2015-04-10)
changeset 6000741a117825097
parent 60006 fd9191f0d323
child 60008 dfbd51a5eab1
make SML/NJ more happy;
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Apr 10 23:56:41 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Apr 10 23:58:07 2015 +0200
     1.3 @@ -617,7 +617,7 @@
     1.4  
     1.5  fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy =
     1.6    let
     1.7 -    val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
     1.8 +    val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes);
     1.9      val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
    1.10  
    1.11      val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)