# HG changeset patch
# User wenzelm
# Date 1570713520 -7200
# Node ID 63c60df79187cb6ef77cf5c278b2941c81ee8d3e
# Parent  3c215bdf4ab67bb6f9b79f51cf62573adb7c7cb7
tuned;

diff -r 3c215bdf4ab6 -r 63c60df79187 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Oct 10 15:10:07 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Oct 10 15:18:40 2019 +0200
@@ -255,20 +255,22 @@
     val defs' = map (Logic.dest_equals o
       map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
     val defnames = map Thm.derivation_name defs;
-    val f = if not r then I else
-      let
-        val cnames = map (fst o dest_Const o fst) defs';
-        val thms = Proofterm.fold_proof_atoms true
-          (fn PThm ({name, prop, ...}, _) =>
-              if member (op =) defnames name orelse
-                not (exists_Const (member (op =) cnames o #1) prop)
-              then I
-              else cons (name, SOME prop)
-            | _ => I) [prf] [];
-      in Proofterm.expand_proof thy thms end;
+    val prf' =
+      if r then
+        let
+          val cnames = map (fst o dest_Const o fst) defs';
+          val thms = Proofterm.fold_proof_atoms true
+            (fn PThm ({name, prop, ...}, _) =>
+                if member (op =) defnames name orelse
+                  not (exists_Const (member (op =) cnames o #1) prop)
+                then I
+                else cons (name, SOME prop)
+              | _ => I) [prf] [];
+        in Proofterm.expand_proof thy thms prf end
+      else prf;
   in
     rewrite_terms (Pattern.rewrite_term thy defs' [])
-      (fst (insert_refl defnames [] (f prf)))
+      (fst (insert_refl defnames [] prf'))
   end;