tuned signature;
authorwenzelm
Mon, 19 Aug 2019 20:08:12 +0200
changeset 70765 7bb2bbb3ccd6
parent 70764 ed651a58afe4
child 70766 5a8e3e4b3760
tuned signature;
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;