# HG changeset patch # User wenzelm # Date 1566306456 -7200 # Node ID 38cc9b2c5a94f34a4d4243ae27d632296a0b484c # Parent 8214aa5d56505dff64fc152591593205579fb051 tuned; diff -r 8214aa5d5650 -r 38cc9b2c5a94 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Aug 20 15:01:45 2019 +0200 +++ b/src/Pure/proofterm.ML Tue Aug 20 15:07:36 2019 +0200 @@ -205,9 +205,11 @@ Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy}; type oracle = string * term option; +val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord); val oracle_prop = the_default Term.dummy; type thm = serial * thm_node; +val thm_ord : thm ord = fn ((i, _), (j, _)) => int_ord (j, i); exception MIN_PROOF; @@ -287,9 +289,6 @@ (* proof body *) -val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord); -fun thm_ord ((i, _): thm, (j, _): thm) = int_ord (j, i); - val unions_oracles = Ord_List.unions oracle_ord; val unions_thms = Ord_List.unions thm_ord;