--- 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 =
--- 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,