# HG changeset patch
# User wenzelm
# Date 1566307447 -7200
# Node ID 1d239ebba0e3b7a658a351c91e16ee3ef606abd9
# Parent  78426ea26f125e4d03c330557e3036f666b13929
tuned;

diff -r 78426ea26f12 -r 1d239ebba0e3 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 20 15:12:06 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 15:24:07 2019 +0200
@@ -209,7 +209,7 @@
 val oracle_prop = the_default Term.dummy;
 
 type thm = serial * thm_node;
-val thm_ord : thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
+val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
 exception MIN_PROOF;
 
diff -r 78426ea26f12 -r 1d239ebba0e3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Aug 20 15:12:06 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 20 15:24:07 2019 +0200
@@ -710,7 +710,7 @@
 
 (* inference rules *)
 
-fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
+val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);
 
 fun deriv_rule2 f
     (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})