Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 58634 9f10d82e8188
parent 56245 84fc7dfa3cd4
child 59058 a78612c67ec0 
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -439,7 +439,7 @@
                 s_let Ts "l" (n + 1) dataT bool_T
                       (fn t1 =>
                           discriminate_value hol_ctxt x t1 ::
-                          map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
+                          @{map 3} (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
                           |> foldr1 s_conj) t1
             else
               raise SAME ()
isabelle