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'