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.
guard constraints by record_proofs=1, until performance implications have become more clear;
authorwenzelm
Sat, 03 Aug 2019 16:17:16 +0200
changeset 70463 d6622add8b54
parent 70462 185c63c40ad7
child 70464 2d6a489adb01
guard constraints by record_proofs=1, until performance implications have become more clear;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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'
isabelle