# HG changeset patch
# User wenzelm
# Date 1564841836 -7200
# Node ID d6622add8b54f22461e9782815a580dca87d8a09
# Parent  185c63c40ad744321182f3a0a3d5e1bd0e67d0c7
guard constraints by record_proofs=1, until performance implications have become more clear;

diff -r 185c63c40ad7 -r d6622add8b54 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 03 16:10:34 2019 +0200
+++ b/src/Pure/thm.ML	Sat Aug 03 16:17:16 2019 +0200
@@ -382,6 +382,7 @@
 fun insert_constraints thy (T, S) =
   let
     val ignored =
+      ! Proofterm.proofs < 1 orelse
       S = [] orelse
         (case T of
           TFree (_, S') => S = S'