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/coinduction.ML
changeset 58634 9f10d82e8188
parent 58002 0ed1e999a0fb
child 58814 4c0ad4162cb7 
--- a/src/HOL/Tools/coinduction.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/coinduction.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -73,7 +73,7 @@
           val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
             |>> (fn names => Variable.variant_fixes names names_ctxt) ;
           val eqs =
-            map3 (fn name => fn T => fn (_, rhs) =>
+            @{map 3} (fn name => fn T => fn (_, rhs) =>
               HOLogic.mk_eq (Free (name, T), rhs))
             names Ts raw_eqs;
           val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
isabelle