# HG changeset patch
# User wenzelm
# Date 1564127412 -7200
# Node ID 913b4afb6ac20ac8a73937a97a73d48e30b35ac8
# Parent  64ead6de6212643f14a46d8e14e8dc5c66e16054
more explicit type proof_serial;

diff -r 64ead6de6212 -r 913b4afb6ac2 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jul 26 09:35:02 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Jul 26 09:50:12 2019 +0200
@@ -9,6 +9,7 @@
 signature BASIC_PROOFTERM =
 sig
   type thm_node
+  type proof_serial = int
   datatype proof =
      MinProof
    | PBound of int
@@ -20,10 +21,10 @@
    | PAxm of string * term * typ list option
    | OfClass of typ * class
    | Oracle of string * term * typ list option
-   | PThm of serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
+   | PThm of proof_serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
   and proof_body = PBody of
     {oracles: (string * term) Ord_List.T,
-     thms: (serial * thm_node) Ord_List.T,
+     thms: (proof_serial * thm_node) Ord_List.T,
      proof: proof}
   val %> : proof * term -> proof
 end;
@@ -32,7 +33,7 @@
 sig
   include BASIC_PROOFTERM
   val proofs: int Unsynchronized.ref
-  type pthm = serial * thm_node
+  type pthm = proof_serial * thm_node
   type oracle = string * term
   val proof_of: proof_body -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
@@ -41,7 +42,8 @@
   val thm_node_body: thm_node -> proof_body future
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
-  val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+  val fold_body_thms:
+    ({serial: proof_serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
   val consolidate: proof_body list -> unit
   val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
@@ -153,6 +155,7 @@
   val forall_intr_vfs_prf: term -> proof -> proof
   val clean_proof: theory -> proof -> proof
 
+  val proof_serial: unit -> proof_serial
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> sort list -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
@@ -167,6 +170,8 @@
 
 (** datatype proof **)
 
+type proof_serial = int;
+
 datatype proof =
    MinProof
  | PBound of int
@@ -178,16 +183,16 @@
  | PAxm of string * term * typ list option
  | OfClass of typ * class
  | Oracle of string * term * typ list option
- | PThm of serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
+ | PThm of proof_serial * ((string * term * typ list option * (proof -> proof)) * proof_body future)
 and proof_body = PBody of
   {oracles: (string * term) Ord_List.T,
-   thms: (serial * thm_node) Ord_List.T,
+   thms: (proof_serial * thm_node) Ord_List.T,
    proof: proof}
 and thm_node =
   Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
 
 type oracle = string * term;
-type pthm = serial * thm_node;
+type pthm = proof_serial * thm_node;
 
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;