# HG changeset patch
# User wenzelm
# Date 1566238092 -7200
# Node ID 7bb2bbb3ccd66d907bcf2a923bf8d31231575bbe
# Parent  ed651a58afe499b5bb1fc9abb220317a2c91568f
tuned signature;

diff -r ed651a58afe4 -r 7bb2bbb3ccd6 src/Pure/proofterm.ML
--- 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;