# HG changeset patch
# User wenzelm
# Date 1565725928 -7200
# Node ID 095e6459d3dac028ae7f2b272702305243d0b18a
# Parent  bb18c7ac9cff8db2531659e135a815175de5b40b
tuned;

diff -r bb18c7ac9cff -r 095e6459d3da src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Tue Aug 13 21:18:26 2019 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Tue Aug 13 21:52:08 2019 +0200
@@ -66,10 +66,12 @@
       Data.prove_conv [Data.norm_tac ctxt'] ctxt' prems
         (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
   in
-    Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt')
-      (Data.prove_conv
-         [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.cancel] 1,
-          Data.numeral_simp_tac ctxt'] ctxt' prems (t', rhs))
+    Data.prove_conv
+       [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.cancel] 1,
+        Data.numeral_simp_tac ctxt'] ctxt' prems (t', rhs)
+    |> Option.map
+      (Data.simplify_meta_eq ctxt' #>
+        singleton (Variable.export ctxt' ctxt))
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE
diff -r bb18c7ac9cff -r 095e6459d3da src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Tue Aug 13 21:18:26 2019 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Tue Aug 13 21:52:08 2019 +0200
@@ -88,21 +88,22 @@
         else Data.prove_conv [Data.norm_tac ctxt'] ctxt' prems
           (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2')))
   in
-    Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt')
-      (if n2 <= n1 then
-         Data.prove_conv
-           [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add1] 1,
-            Data.numeral_simp_tac ctxt'] ctxt' prems
-           (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
-       else
-         Data.prove_conv
-           [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add2] 1,
-            Data.numeral_simp_tac ctxt'] ctxt' prems
-           (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
+    (if n2 <= n1 then
+       Data.prove_conv
+         [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add1] 1,
+          Data.numeral_simp_tac ctxt'] ctxt' prems
+         (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
+     else
+       Data.prove_conv
+         [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add2] 1,
+          Data.numeral_simp_tac ctxt'] ctxt' prems
+         (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
+    |> Option.map
+      (Data.simplify_meta_eq ctxt' #>
+        singleton (Variable.export ctxt' ctxt))
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE
        | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
                              Undeclared type constructor "Numeral.bin"*)
-
 end;
diff -r bb18c7ac9cff -r 095e6459d3da src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Tue Aug 13 21:18:26 2019 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Tue Aug 13 21:52:08 2019 +0200
@@ -80,11 +80,13 @@
       else Data.prove_conv [Data.norm_tac ctxt'] ctxt'
         (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
   in
-    Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt')
-      (Data.prove_conv
-         [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.left_distrib] 1,
-          Data.numeral_simp_tac ctxt'] ctxt'
-         (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
+    Data.prove_conv
+       [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.left_distrib] 1,
+        Data.numeral_simp_tac ctxt'] ctxt'
+       (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))
+    |> Option.map
+      (Data.simplify_meta_eq ctxt' #>
+        singleton (Variable.export ctxt' ctxt))
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE