# HG changeset patch
# User wenzelm
# Date 1570712436 -7200
# Node ID 7000868c6098d36e45aa69c528264cc8087b4edb
# Parent  c6f2a73987cdf7f05ec0edccf4d2c0332c8cbeba
clarified modules;

diff -r c6f2a73987cd -r 7000868c6098 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 10 14:55:26 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 10 15:00:36 2019 +0200
@@ -103,6 +103,7 @@
   val term_of_proof: proof -> term
 
   (*proof terms for specific inference rules*)
+  val trivial_proof: proof
   val implies_intr_proof: term -> proof -> proof
   val implies_intr_proof': term -> proof -> proof
   val forall_intr_proof: string * term -> typ option -> proof -> proof
@@ -845,6 +846,11 @@
 
 (** inference rules **)
 
+(* trivial implication *)
+
+val trivial_proof = AbsP ("H", NONE, PBound 0);
+
+
 (* implication introduction *)
 
 fun gen_implies_intr_proof f h prf =
diff -r c6f2a73987cd -r 7000868c6098 src/Pure/thm.ML
--- 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,