Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
record sort constraints unconditionally: minimal performance implications;
authorwenzelm
Sun, 11 Aug 2019 22:36:34 +0200
changeset 70503 f0b2635ee17f
parent 70502 b053c9ed0b0a
child 70504 8d4abdbc6de9
child 70505 1881fb38a1ef
record sort constraints unconditionally: minimal performance implications;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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'
isabelle