--- a/src/Pure/thm.ML Sat Aug 10 17:09:20 2019 +0200
+++ b/src/Pure/thm.ML Sun Aug 11 22:36:34 2019 +0200
@@ -382,7 +382,6 @@
fun insert_constraints thy (T, S) =
let
val ignored =
- ! Proofterm.proofs < 1 orelse
S = [] orelse
(case T of
TFree (_, S') => S = S'