# HG changeset patch
# User wenzelm
# Date 1473705088 -7200
# Node ID 0f5e735e364029fd14f1fe5cb48b0b743643d85b
# Parent  0883c1cc655c0de34a7d19033bdfcbcdb425f0cf
tuned;

diff -r 0883c1cc655c -r 0f5e735e3640 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Sep 12 20:24:42 2016 +0200
+++ b/src/Pure/thm.ML	Mon Sep 12 20:31:28 2016 +0200
@@ -1410,7 +1410,7 @@
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
       Thm (deriv_rule1
-          ((if Envir.is_empty env then I else (Proofterm.norm_proof' env)) o
+          ((if Envir.is_empty env then I else Proofterm.norm_proof' env) o
             Proofterm.assumption_proof Bs Bi n) der,
        {tags = [],
         maxidx = Envir.maxidx_of env,