--- a/src/Pure/proofterm.ML Mon Aug 19 20:00:29 2019 +0200
+++ b/src/Pure/proofterm.ML Mon Aug 19 20:08:12 2019 +0200
@@ -6,7 +6,7 @@
infix 8 % %% %>;
-signature BASIC_PROOFTERM =
+signature PROOFTERM =
sig
type thm_node
type thm_header =
@@ -30,11 +30,6 @@
thms: (serial * thm_node) Ord_List.T,
proof: proof}
val %> : proof * term -> proof
-end;
-
-signature PROOFTERM =
-sig
- include BASIC_PROOFTERM
val proofs: int Unsynchronized.ref
exception MIN_PROOF
type pthm = serial * thm_node
@@ -2222,5 +2217,11 @@
end;
-structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
+structure Basic_Proofterm =
+struct
+ datatype proof = datatype Proofterm.proof
+ datatype proof_body = datatype Proofterm.proof_body
+ val op %> = Proofterm.%>
+end;
+
open Basic_Proofterm;