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.
make SML/NJ more happy;
authorwenzelm
Fri, 10 Apr 2015 23:58:07 +0200
changeset 60007 41a117825097
parent 60006 fd9191f0d323
child 60008 dfbd51a5eab1
make SML/NJ more happy;
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle