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/semiring_normalizer.ML
changeset 59058 a78612c67ec0
parent 58826 2ed2eaabe3df
child 59321 2b40fb12b09d 
--- a/src/HOL/Tools/semiring_normalizer.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -145,11 +145,11 @@
       val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
       val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
       val ((clx, crx), (cly, cry)) =
-        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop;
       val ((ca, cb), (cc, cd)) =
-        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
+        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop;
       val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
-      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
+      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_arg;
 
       val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
       val semiring = (sr_ops, sr_rules');
isabelle