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/BNF/bnf_fp_n2m_tactics.ML
changeset 58634 9f10d82e8188
parent 58375 7b92932ffea5
child 58963 26bf09b95dda 
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -32,7 +32,7 @@
     val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
     val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
     val C_IH_monos =
-      map3 (fn C_IH => fn mono => fn unfold =>
+      @{map 3} (fn C_IH => fn mono => fn unfold =>
         (mono RSN (2, @{thm vimage2p_mono}), C_IH)
         |> fp = Greatest_FP ? swap
         |> op RS
isabelle