# HG changeset patch
# User wenzelm
# Date 1565555794 -7200
# Node ID f0b2635ee17f7023272df21968013bc9b4274f89
# Parent  b053c9ed0b0a40893929e1e9c57ddfb41944c62f
record sort constraints unconditionally: minimal performance implications;

diff -r b053c9ed0b0a -r f0b2635ee17f src/Pure/thm.ML
--- 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'