Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm.ML
changeset 70824 7000868c6098
parent 70822 22e2f5acc0b4
child 70825 3c215bdf4ab6 
--- a/src/Pure/thm.ML	Thu Oct 10 14:55:26 2019 +0200
+++ b/src/Pure/thm.ML	Thu Oct 10 15:00:36 2019 +0200
@@ -1631,7 +1631,7 @@
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
-    Thm (deriv_rule0 (fn () => Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
+    Thm (deriv_rule0 (fn () => Proofterm.trivial_proof),
      {cert = cert,
       tags = [],
       maxidx = maxidx,
isabelle