# HG changeset patch
# User wenzelm
# Date 1566325401 -7200
# Node ID a56b4e59bfd146640f3a1faf2d21276a5d48b305
# Parent  eecade21bc6a8871f368570c413618e7c40a21aa# Parent  a896257a3f07c4993dbe9d8295820d67bfc53293
merged

diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -104,7 +104,7 @@
     * string * (string * 'd list) list) list * string list
   val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
     ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
-  val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
+  val vampire_step_name_ord : (string * 'a) ord
   val core_of_agsyhol_proof :  string -> string list option
 end;
 
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -7,7 +7,7 @@
 signature ATP_ATOM =
 sig
   type key
-  val ord : key * key -> order
+  val ord : key ord
   val string_of : key -> string
 end;
 
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -92,7 +92,7 @@
   val untuple : (nut -> 'a) -> nut -> 'a list
   val add_free_and_const_names :
     nut -> nut list * nut list -> nut list * nut list
-  val name_ord : (nut * nut) -> order
+  val name_ord : nut ord
   val the_name : 'a NameTable.table -> nut -> 'a
   val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
   val nut_from_term : hol_context -> op2 -> term -> nut
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -10,7 +10,7 @@
   (* mode *)
   datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
   val eq_mode : mode * mode -> bool
-  val mode_ord: mode * mode -> order
+  val mode_ord: mode ord
   val list_fun_mode : mode list -> mode
   val strip_fun_mode : mode -> mode list
   val dest_fun_mode : mode -> mode list
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -24,7 +24,7 @@
 
   val no_label : label
 
-  val label_ord : label * label -> order
+  val label_ord : label ord
   val string_of_label : label -> string
   val sort_facts : facts -> facts
 
@@ -39,7 +39,7 @@
 
   structure Canonical_Label_Tab : TABLE
 
-  val canonical_label_ord : (label * label) -> order
+  val canonical_label_ord : label ord
 
   val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
   val chain_isar_proof : isar_proof -> isar_proof
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -48,7 +48,7 @@
     (real * (('a * real) list * 'a list)) list -> 'a list
   val nickname_of_thm : thm -> string
   val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
-  val crude_thm_ord : Proof.context -> thm * thm -> order
+  val crude_thm_ord : Proof.context -> thm ord
   val thm_less : thm * thm -> bool
   val goal_of_thm : theory -> thm -> thm
   val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -38,7 +38,7 @@
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
-  val play_outcome_ord : play_outcome * play_outcome -> order
+  val play_outcome_ord : play_outcome ord
   val one_line_proof_text : Proof.context -> int -> one_line_params -> string
 end;
 
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/groebner.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -10,7 +10,7 @@
     (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
     conv ->  conv ->
      {ring_conv: Proof.context -> conv,
-     simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
+     simple_ideal: cterm list -> cterm -> cterm ord -> cterm list,
      multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
      poly_eq_ss: simpset, unwind_conv: Proof.context -> conv}
   val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
diff -r eecade21bc6a -r a56b4e59bfd1 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -18,21 +18,19 @@
     local_theory -> local_theory
 
   val semiring_normalize_conv: Proof.context -> conv
-  val semiring_normalize_ord_conv: Proof.context -> (cterm * cterm -> order) -> conv
+  val semiring_normalize_ord_conv: Proof.context -> cterm ord -> conv
   val semiring_normalize_wrapper: Proof.context -> entry -> conv
-  val semiring_normalize_ord_wrapper: Proof.context -> entry
-    -> (cterm * cterm -> order) -> conv
+  val semiring_normalize_ord_wrapper: Proof.context -> entry -> cterm ord -> conv
   val semiring_normalizers_conv: cterm list -> cterm list * thm list
     -> cterm list * thm list -> cterm list * thm list ->
-      (cterm -> bool) * conv * conv * conv -> (cterm * cterm -> order) ->
+      (cterm -> bool) * conv * conv * conv -> cterm ord ->
         {add: Proof.context -> conv,
          mul: Proof.context -> conv,
          neg: Proof.context -> conv,
          main: Proof.context -> conv,
          pow: Proof.context -> conv,
          sub: Proof.context -> conv}
-  val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
-    (cterm * cterm -> order) ->
+  val semiring_normalizers_ord_wrapper:  Proof.context -> entry -> cterm ord ->
       {add: Proof.context -> conv,
        mul: Proof.context -> conv,
        neg: Proof.context -> conv,
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/General/heap.ML
--- a/src/Pure/General/heap.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/heap.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -20,7 +20,7 @@
   val upto: elem -> T -> elem list * T
 end;
 
-functor Heap(type elem val ord: elem * elem -> order): HEAP =
+functor Heap(type elem val ord: elem ord): HEAP =
 struct
 
 
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/name_space.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -16,14 +16,14 @@
   val markup_def: T -> string -> Markup.T
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
-  val entry_ord: T -> string * string -> order
+  val entry_ord: T -> string ord
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val names_long: bool Config.T
   val names_short: bool Config.T
   val names_unique: bool Config.T
   val extern: Proof.context -> T -> string -> xstring
-  val extern_ord: Proof.context -> T -> string * string -> order
+  val extern_ord: Proof.context -> T -> string ord
   val extern_shortest: Proof.context -> T -> string -> xstring
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val pretty: Proof.context -> T -> string -> Pretty.T
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/rat.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -13,7 +13,7 @@
   val dest: rat -> int * int
   val string_of_rat: rat -> string
   val signed_string_of_rat: rat -> string
-  val ord: rat * rat -> order
+  val ord: rat ord
   val le: rat -> rat -> bool
   val lt: rat -> rat -> bool
   val sign: rat -> order
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/General/table.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -8,7 +8,7 @@
 signature KEY =
 sig
   type key
-  val ord: key * key -> order
+  val ord: key ord
 end;
 
 signature TABLE =
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -10,9 +10,9 @@
 sig
   datatype recursion =
     Primrec of string list | Recdef | Primcorec of string list | Corec | Unknown_Recursion
-  val recursion_ord: recursion * recursion -> order
+  val recursion_ord: recursion ord
   datatype rough_classification = Equational of recursion | Inductive | Co_Inductive | Unknown
-  val rough_classification_ord: rough_classification * rough_classification -> order
+  val rough_classification_ord: rough_classification ord
   val equational_primrec: string list -> rough_classification
   val equational_recdef: rough_classification
   val equational_primcorec: string list -> rough_classification
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -173,6 +173,21 @@
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
 
+fun make_proof_body prf =
+  let
+    val (oracles, thms) =
+      ([prf], ([], [])) |-> Proofterm.fold_proof_atoms false
+        (fn Oracle (name, prop, _) => apfst (cons (name, prop))
+          | PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
+          | _ => I);
+    val body =
+      PBody
+       {oracles = Ord_List.make Proofterm.oracle_ord oracles,
+        thms = Ord_List.make Proofterm.thm_ord thms,
+        proof = prf};
+  in Proofterm.thm_body body end;
+
+
 
 (**** theory data ****)
 
@@ -625,11 +640,10 @@
                       Proofterm.thm_header (serial ()) pos theory_name
                         (corr_name name vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
-                    val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
                     val corr_prf' =
                       Proofterm.proof_combP
                         (Proofterm.proof_combt
-                          (PThm (corr_header, corr_body), vfs_of corr_prop),
+                          (PThm (corr_header, make_proof_body corr_prf), vfs_of corr_prop),
                             map PBound (length shyps - 1 downto 0)) |>
                       fold_rev Proofterm.forall_intr_proof'
                         (map (get_var_type corr_prop) (vfs_of prop)) |>
@@ -746,10 +760,9 @@
                       Proofterm.thm_header (serial ()) pos theory_name
                         (corr_name s vs') corr_prop
                         (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
-                    val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
                     val corr_prf'' =
                       Proofterm.proof_combP (Proofterm.proof_combt
-                        (PThm (corr_header, corr_body), vfs_of corr_prop),
+                        (PThm (corr_header, make_proof_body corr_prf), vfs_of corr_prop),
                              map PBound (length shyps - 1 downto 0)) |>
                       fold_rev Proofterm.forall_intr_proof'
                         (map (get_var_type corr_prop) (vfs_of prop)) |>
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -32,7 +32,7 @@
   val dummy: token
   val literal: string -> token
   val is_literal: token -> bool
-  val tokens_match_ord: token * token -> order
+  val tokens_match_ord: token ord
   val mk_eof: Position.T -> token
   val eof: token
   val is_eof: token -> bool
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -255,13 +255,20 @@
         val {pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
 
-    val encode_thm = clean_thm #> (fn thm =>
-      standard_prop Name.context
-        (Thm.extra_shyps thm)
-        (Thm.full_prop_of thm)
-        (try Thm.reconstruct_proof_of thm) |>
-      let open XML.Encode Term_XML.Encode
-      in pair encode_prop (option Proofterm.encode_full) end);
+    fun encode_thm raw_thm =
+      let
+        val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm);
+        val thm = clean_thm raw_thm;
+        val (prop, proof) =
+          standard_prop Name.context
+            (Thm.extra_shyps thm)
+            (Thm.full_prop_of thm)
+            (try Thm.reconstruct_proof_of thm);
+      in
+        (prop, (deps, proof)) |>
+          let open XML.Encode Term_XML.Encode
+          in pair encode_prop (pair (list string) (option Proofterm.encode_full)) end
+      end;
 
     fun export_thms thms =
       let val elems =
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 20 20:23:21 2019 +0200
@@ -327,23 +327,23 @@
 
   /* theorems */
 
-  sealed case class Thm(entity: Entity, prop: Prop, proof: Option[Term.Proof])
+  sealed case class Thm(entity: Entity, prop: Prop, deps: List[String], proof: Option[Term.Proof])
   {
     def cache(cache: Term.Cache): Thm =
-      Thm(entity.cache(cache), prop.cache(cache), proof.map(cache.proof _))
+      Thm(entity.cache(cache), prop.cache(cache), deps.map(cache.string _), proof.map(cache.proof _))
   }
 
   def read_thms(provider: Export.Provider): List[Thm] =
     provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.THM, tree)
-        val (prop, prf) =
+        val (prop, (deps, prf)) =
         {
           import XML.Decode._
           import Term_XML.Decode._
-          pair(decode_prop _, option(proof))(body)
+          pair(decode_prop _, pair(list(string), option(proof)))(body)
         }
-        Thm(entity, prop, prf)
+        Thm(entity, prop, deps, prf)
       })
 
   def read_proof(
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -10,6 +10,7 @@
   val all_oracles: thm list -> Proofterm.oracle list
   val has_skip_proof: thm list -> bool
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
+  val thm_deps: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) list
   val thm_deps_cmd: theory -> thm list -> unit
   val unused_thms_cmd: theory list * theory list -> (string * thm) list
 end;
@@ -20,7 +21,16 @@
 (* oracles *)
 
 fun all_oracles thms =
-  Proofterm.all_oracles_of (map Thm.proof_body_of thms);
+  let
+    fun collect (PBody {oracles, thms, ...}) =
+      (if null oracles then I else apfst (cons oracles)) #>
+      (tap Proofterm.join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
+        if Inttab.defined seen i then (res, seen)
+        else
+          let val body = Future.join (Proofterm.thm_node_body thm_node)
+          in collect body (res, Inttab.update (i, ()) seen) end));
+    val bodies = map Thm.proof_body_of thms;
+  in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end;
 
 fun has_skip_proof thms =
   all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>);
@@ -35,6 +45,26 @@
   in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;
 
 
+(* thm_deps *)
+
+fun thm_deps thy =
+  let
+    val lookup = Global_Theory.lookup_thm_id thy;
+    fun deps (i, thm_node) res =
+      if Inttab.defined res i then res
+      else
+        let val thm_id = Proofterm.thm_id (i, thm_node) in
+          (case lookup thm_id of
+            SOME thm_name => Inttab.update (i, (thm_id, thm_name)) res
+          | NONE => fold deps (Proofterm.thm_node_thms thm_node) res)
+        end;
+  in
+    fn thm =>
+      fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty
+      |> Inttab.dest |> map #2
+  end;
+
+
 (* thm_deps_cmd *)
 
 fun thm_deps_cmd thy thms =
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/context.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -33,7 +33,7 @@
   val timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
-  val theory_id_ord: theory_id * theory_id -> order
+  val theory_id_ord: theory_id ord
   val theory_id_long_name: theory_id -> string
   val theory_id_name: theory_id -> string
   val theory_long_name: theory -> string
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/defs.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -11,7 +11,7 @@
   datatype item_kind = Const | Type
   type item = item_kind * string
   type entry = item * typ list
-  val item_kind_ord: item_kind * item_kind -> order
+  val item_kind_ord: item_kind ord
   val plain_args: typ list -> bool
   type context = Proof.context * (Name_Space.T * Name_Space.T)
   val global_context: theory -> context
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/global_theory.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -15,7 +15,7 @@
   val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
   val dest_thm_names: theory -> (serial * Thm_Name.T) list
   val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
-  val lookup_thm: theory -> thm -> Thm_Name.T option
+  val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
@@ -126,8 +126,15 @@
   in lookup end;
 
 fun lookup_thm thy =
-  let val lookup = lookup_thm_id thy
-  in fn thm => (case Thm.derivation_id thm of NONE => NONE | SOME thm_id => lookup thm_id) end;
+  let val lookup = lookup_thm_id thy in
+    fn thm =>
+      (case Thm.derivation_id thm of
+        NONE => NONE
+      | SOME thm_id =>
+          (case lookup thm_id of
+            NONE => NONE
+          | SOME thm_name => SOME (thm_id, thm_name)))
+  end;
 
 val _ =
   Theory.setup (Theory.at_end (fn thy =>
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/library.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -185,24 +185,25 @@
   val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
 
   (*orders*)
+  type 'a ord = 'a * 'a -> order
   val is_equal: order -> bool
   val is_less: order -> bool
   val is_less_equal: order -> bool
   val is_greater: order -> bool
   val is_greater_equal: order -> bool
   val rev_order: order -> order
-  val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
-  val bool_ord: bool * bool -> order
-  val int_ord: int * int -> order
-  val string_ord: string * string -> order
-  val fast_string_ord: string * string -> order
+  val make_ord: ('a * 'a -> bool) -> 'a ord
+  val bool_ord: bool ord
+  val int_ord: int ord
+  val string_ord: string ord
+  val fast_string_ord: string ord
   val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
   val <<< : ('a -> order) * ('a -> order) -> 'a -> order
   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
   val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
-  val sort: ('a * 'a -> order) -> 'a list -> 'a list
-  val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list
+  val sort: 'a ord -> 'a list -> 'a list
+  val sort_distinct: 'a ord -> 'a list -> 'a list
   val sort_strings: string list -> string list
   val sort_by: ('a -> string) -> 'a list -> 'a list
   val tag_list: int -> 'a list -> (int * 'a) list
@@ -896,6 +897,8 @@
 
 (** orders **)
 
+type 'a ord = 'a * 'a -> order;
+
 fun is_equal ord = ord = EQUAL;
 fun is_less ord = ord = LESS;
 fun is_less_equal ord = ord = LESS orelse ord = EQUAL;
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/more_thm.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -40,9 +40,9 @@
   val dest_equals_rhs: cterm -> cterm
   val lhs_of: thm -> cterm
   val rhs_of: thm -> cterm
-  val fast_term_ord: cterm * cterm -> order
-  val term_ord: cterm * cterm -> order
-  val thm_ord: thm * thm -> order
+  val fast_term_ord: cterm ord
+  val term_ord: cterm ord
+  val thm_ord: thm ord
   val cterm_cache: (cterm -> 'a) -> cterm -> 'a
   val thm_cache: (thm -> 'a) -> thm -> 'a
   val is_reflexive: thm -> bool
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -8,11 +8,11 @@
 
 signature PROOFTERM =
 sig
-  type thm_node
   type thm_header =
     {serial: serial, pos: Position.T list, theory_name: string, name: string,
       prop: term, types: typ list option}
   type thm_body
+  type thm_node
   datatype proof =
      MinProof
    | PBound of int
@@ -29,34 +29,33 @@
     {oracles: (string * term option) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
      proof: proof}
-  val %> : proof * term -> proof
-  val proofs: int Unsynchronized.ref
+  type oracle = string * term option
+  type thm = serial * thm_node
   exception MIN_PROOF
-  type pthm = serial * thm_node
-  type oracle = string * term option
   val proof_of: proof_body -> proof
+  val join_proof: proof_body future -> proof
   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
   val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
     thm_header
   val thm_body: proof_body -> thm_body
   val thm_body_proof_raw: thm_body -> proof
   val thm_body_proof_open: thm_body -> proof
+  val thm_node_theory_name: thm_node -> string
   val thm_node_name: thm_node -> string
   val thm_node_prop: thm_node -> term
   val thm_node_body: thm_node -> proof_body future
-  val join_proof: proof_body future -> proof
+  val thm_node_thms: thm_node -> thm list
+  val join_thms: thm list -> proof_body list
+  val consolidate: proof_body list -> unit
+  val make_thm: thm_header -> thm_body -> thm
   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) ->
     proof_body list -> 'a -> 'a
-  val consolidate: proof_body list -> unit
-
-  val oracle_ord: oracle * oracle -> order
-  val thm_ord: pthm * pthm -> order
+  val oracle_ord: oracle ord
+  val thm_ord: thm ord
   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
-  val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
-  val all_oracles_of: proof_body list -> oracle Ord_List.T
-  val approximate_proof_body: proof -> proof_body
+  val unions_thms: thm Ord_List.T list -> thm Ord_List.T
   val no_proof_body: proof -> proof_body
   val no_thm_proofs: proof -> proof
   val no_body_proofs: proof -> proof
@@ -67,7 +66,10 @@
   val decode: proof XML.Decode.T
   val decode_body: proof_body XML.Decode.T
 
+  val %> : proof * term -> proof
+
   (*primitive operations*)
+  val proofs: int Unsynchronized.ref
   val proofs_enabled: unit -> bool
   val atomic_proof: proof -> bool
   val compact_proof: proof -> bool
@@ -165,12 +167,13 @@
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
-    term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof
+    term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
   val unconstrain_thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> sort list -> term ->
-    (serial * proof_body future) list -> proof_body -> pthm * proof
+    (serial * proof_body future) list -> proof_body -> thm * proof
   val get_approximative_name: sort list -> term list -> term -> proof -> string
   type thm_id = {serial: serial, theory_name: string}
+  val thm_id: thm -> thm_id
   val get_id: sort list -> term list -> term -> proof -> thm_id option
 end
 
@@ -202,14 +205,18 @@
 and thm_body =
   Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future}
 and thm_node =
-  Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
+  Thm_Node of {theory_name: string, 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;
 
-type oracle = string * term option;
-val oracle_prop = the_default Term.dummy;
-
-type pthm = serial * thm_node;
 
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
@@ -229,25 +236,30 @@
 fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body);
 
 fun rep_thm_node (Thm_Node args) = args;
+val thm_node_theory_name = #theory_name o rep_thm_node;
 val thm_node_name = #name o rep_thm_node;
 val thm_node_prop = #prop o rep_thm_node;
 val thm_node_body = #body o rep_thm_node;
+val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
 val thm_node_consolidate = #consolidate o rep_thm_node;
 
-fun join_thms (thms: pthm list) =
+fun join_thms (thms: thm list) =
   Future.joins (map (thm_node_body o #2) thms);
 
 val consolidate =
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
   #> Lazy.consolidate #> map Lazy.force #> ignore;
 
-fun make_thm_node name prop body =
-  Thm_Node {name = name, prop = prop, body = body,
+fun make_thm_node theory_name name prop body =
+  Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
     consolidate =
       Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
         let val PBody {thms, ...} = Future.join body
         in consolidate (join_thms thms) end)};
 
+fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+  (serial, make_thm_node theory_name name prop body);
+
 
 (* proof atoms *)
 
@@ -283,37 +295,9 @@
 
 (* proof body *)
 
-val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
-fun thm_ord ((i, _): pthm, (j, _): pthm) = int_ord (j, i);
-
 val unions_oracles = Ord_List.unions oracle_ord;
 val unions_thms = Ord_List.unions thm_ord;
 
-fun all_oracles_of bodies =
-  let
-    fun collect (PBody {oracles, thms, ...}) =
-      (if null oracles then I else apfst (cons oracles)) #>
-      (tap join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
-        if Inttab.defined seen i then (res, seen)
-        else
-          let val body = Future.join (thm_node_body thm_node)
-          in collect body (res, Inttab.update (i, ()) seen) end));
-  in fold collect bodies ([], Inttab.empty) |> #1 |> unions_oracles end;
-
-fun approximate_proof_body prf =
-  let
-    val (oracles, thms) = fold_proof_atoms false
-      (fn Oracle (s, prop, _) => apfst (cons (s, prop))
-        | PThm ({serial = i, name, prop, ...}, Thm_Body {body, ...}) =>
-            apsnd (cons (i, make_thm_node name prop body))
-        | _ => I) [prf] ([], []);
-  in
-    PBody
-     {oracles = Ord_List.make oracle_ord oracles,
-      thms = Ord_List.make thm_ord thms,
-      proof = prf}
-  end;
-
 fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
 val no_thm_body = thm_body (no_proof_body MinProof);
 
@@ -361,10 +345,11 @@
       pair (list properties) (pair term (pair (option (list typ)) proof_body))
         (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
 and proof_body (PBody {oracles, thms, proof = prf}) =
-  triple (list (pair string (option term))) (list pthm) proof (oracles, thms, prf)
-and pthm (a, thm_node) =
-  pair int (triple string term proof_body)
-    (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
+  triple (list (pair string (option term))) (list thm) proof (oracles, thms, prf)
+and thm (a, thm_node) =
+  pair int (pair string (pair string (pair term proof_body)))
+    (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
+      (Future.join (thm_node_body thm_node))))));
 
 fun full_proof prf = prf |> variant
  [fn MinProof => ([], []),
@@ -413,11 +398,11 @@
       val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
     in PThm (header, thm_body h) end]
 and proof_body x =
-  let val (a, b, c) = triple (list (pair string (option term))) (list pthm) proof x
+  let val (a, b, c) = triple (list (pair string (option term))) (list thm) proof x
   in PBody {oracles = a, thms = b, proof = c} end
-and pthm x =
-  let val (a, (b, c, d)) = pair int (triple string term proof_body) x
-  in (a, make_thm_node b c (Future.value d)) end;
+and thm x =
+  let val (a, (b, (c, (d, e)))) = pair int (pair string (pair string (pair term proof_body))) x
+  in (a, make_thm_node b c d (Future.value e)) end;
 
 in
 
@@ -429,6 +414,9 @@
 
 (** proof objects with different levels of detail **)
 
+val proofs = Unsynchronized.ref 2;
+fun proofs_enabled () = ! proofs >= 2;
+
 fun atomic_proof prf =
   (case prf of
     Abst _ => false
@@ -1086,9 +1074,6 @@
 
 (** axioms and theorems **)
 
-val proofs = Unsynchronized.ref 2;
-fun proofs_enabled () = ! proofs >= 2;
-
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
 
@@ -2167,10 +2152,10 @@
       if named orelse not (export_enabled ()) then no_export_proof
       else Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1);
 
-    val pthm = (i, make_thm_node name prop1 body');
+    val theory_name = Context.theory_long_name thy;
+    val thm = (i, make_thm_node theory_name name prop1 body');
 
-    val header =
-      thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
+    val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
     val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
     val head = PThm (header, thm_body);
     val proof =
@@ -2179,7 +2164,7 @@
       else
         proof_combP (proof_combt' (head, args),
           map OfClass (#outer_constraints ucontext) @ map Hyp hyps);
-  in (pthm, proof) end;
+  in (thm, proof) end;
 
 in
 
@@ -2209,6 +2194,9 @@
 
 type thm_id = {serial: serial, theory_name: string};
 
+fun thm_id (serial, thm_node) : thm_id =
+  {serial = serial, theory_name = thm_node_theory_name thm_node};
+
 fun get_id shyps hyps prop prf : thm_id option =
   (case get_identity shyps hyps prop prf of
     NONE => NONE
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -82,7 +82,7 @@
       mk_sym: Proof.context -> thm -> thm option,
       mk_eq_True: Proof.context -> thm -> thm option,
       reorient: Proof.context -> term list -> term -> term -> bool},
-    term_ord: term * term -> order,
+    term_ord: term ord,
     subgoal_tac: Proof.context -> int -> tactic,
     loop_tacs: (string * (Proof.context -> int -> tactic)) list,
     solvers: solver list * solver list}
@@ -101,7 +101,7 @@
   val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
   val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
   val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
-  val set_term_ord: (term * term -> order) -> Proof.context -> Proof.context
+  val set_term_ord: term ord -> Proof.context -> Proof.context
   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   val solver: Proof.context -> solver -> int -> tactic
   val default_mk_sym: Proof.context -> thm -> thm option
@@ -268,7 +268,7 @@
       mk_sym: Proof.context -> thm -> thm option,
       mk_eq_True: Proof.context -> thm -> thm option,
       reorient: Proof.context -> term list -> term -> term -> bool},
-    term_ord: term * term -> order,
+    term_ord: term ord,
     subgoal_tac: Proof.context -> int -> tactic,
     loop_tacs: (string * (Proof.context -> int -> tactic)) list,
     solvers: solver list * solver list};
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/simplifier.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -57,7 +57,7 @@
   val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
   val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
   val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
-  val set_term_ord: (term * term -> order) -> Proof.context -> Proof.context
+  val set_term_ord: term ord -> Proof.context -> Proof.context
   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   type trace_ops
   val set_trace_ops: trace_ops -> theory -> theory
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/term_ord.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -15,17 +15,17 @@
 signature TERM_ORD =
 sig
   include BASIC_TERM_ORD
-  val fast_indexname_ord: indexname * indexname -> order
-  val sort_ord: sort * sort -> order
-  val typ_ord: typ * typ -> order
-  val fast_term_ord: term * term -> order
-  val syntax_term_ord: term * term -> order
-  val indexname_ord: indexname * indexname -> order
-  val tvar_ord: (indexname * sort) * (indexname * sort) -> order
-  val var_ord: (indexname * typ) * (indexname * typ) -> order
-  val term_ord: term * term -> order
-  val hd_ord: term * term -> order
-  val term_lpo: (term -> int) -> term * term -> order
+  val fast_indexname_ord: indexname ord
+  val sort_ord: sort ord
+  val typ_ord: typ ord
+  val fast_term_ord: term ord
+  val syntax_term_ord: term ord
+  val indexname_ord: indexname ord
+  val tvar_ord: (indexname * sort) ord
+  val var_ord: (indexname * typ) ord
+  val term_ord: term ord
+  val hd_ord: term ord
+  val term_lpo: (term -> int) -> term ord
   val term_cache: (term -> 'a) -> term -> 'a
 end;
 
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -103,6 +103,7 @@
   val proof_of: thm -> proof
   val consolidate: thm list -> unit
   val future: thm future -> cterm -> thm
+  val thm_deps: thm -> Proofterm.thm Ord_List.T
   val derivation_closed: thm -> bool
   val derivation_name: thm -> string
   val derivation_id: thm -> Proofterm.thm_id option
@@ -371,7 +372,7 @@
 
 local
 
-val constraint_ord : constraint * constraint -> order =
+val constraint_ord : constraint ord =
   Context.theory_id_ord o apply2 (Context.theory_id o #theory)
   <<< Term_Ord.typ_ord o apply2 #typ
   <<< Term_Ord.sort_ord o apply2 #sort;
@@ -710,7 +711,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}})
@@ -736,7 +737,6 @@
 
 (* fulfilled proofs *)
 
-fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
 fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
 
 fun join_promises [] = ()
@@ -933,7 +933,7 @@
 fun union_digest (oracles1, thms1) (oracles2, thms2) =
   (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]);
 
-fun thm_digest (Thm (Deriv {body = Proofterm.PBody {oracles, thms, ...}, ...}, _)) =
+fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
   (oracles, thms);
 
 fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
@@ -963,10 +963,10 @@
             raise THEORY ("solve_constraints: bad theories for theorem\n" ^
               Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys);
 
-        val Deriv {promises, body = Proofterm.PBody {oracles, thms, proof}} = der;
+        val Deriv {promises, body = PBody {oracles, thms, proof}} = der;
         val (oracles', thms') = (oracles, thms)
           |> fold (fold union_digest o constraint_digest) constraints;
-        val body' = Proofterm.PBody {oracles = oracles', thms = thms', proof = proof};
+        val body' = PBody {oracles = oracles', thms = thms', proof = proof};
       in
         Thm (Deriv {promises = promises, body = body'},
           {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
@@ -991,10 +991,19 @@
 fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
   Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
 
+(*identified PThm node*)
 fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
   Proofterm.get_id shyps hyps prop (proof_of thm)
     handle Proofterm.MIN_PROOF => NONE;
 
+(*dependencies of PThm node*)
+fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) =
+      (case (derivation_id thm, thms) of
+        (SOME {serial = i, ...}, [(j, thm_node)]) =>
+          if i = j then Proofterm.thm_node_thms thm_node else thms
+      | _ => thms)
+  | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]);
+
 fun name_derivation name_pos =
   solve_constraints #> (fn thm as Thm (der, args) =>
     let
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/thm_name.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -10,7 +10,7 @@
 signature THM_NAME =
 sig
   type T = string * int
-  val ord: T * T -> order
+  val ord: T ord
   val print: T -> string
   val flatten: T -> string
   val make_list: string -> thm list -> (T * thm) list
diff -r eecade21bc6a -r a56b4e59bfd1 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Pure/variable.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -41,7 +41,7 @@
   val is_improper: Proof.context -> string -> bool
   val is_fixed: Proof.context -> string -> bool
   val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
-  val fixed_ord: Proof.context -> string * string -> order
+  val fixed_ord: Proof.context -> string ord
   val intern_fixed: Proof.context -> string -> string
   val lookup_fixed: Proof.context -> string -> string option
   val revert_fixed: Proof.context -> string -> string
diff -r eecade21bc6a -r a56b4e59bfd1 src/Tools/Argo/argo_expr.ML
--- a/src/Tools/Argo/argo_expr.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/Argo/argo_expr.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -15,11 +15,11 @@
 
   (* indices, equalities, orders *)
   val int_of_kind: kind -> int
-  val con_ord: (string * typ) * (string * typ) -> order
+  val con_ord: (string * typ) ord
   val eq_kind: kind * kind -> bool
-  val kind_ord: kind * kind -> order
+  val kind_ord: kind ord
   val eq_expr: expr * expr -> bool
-  val expr_ord: expr * expr -> order
+  val expr_ord: expr ord
   val dual_expr: expr -> expr -> bool
 
   (* constructors *)
diff -r eecade21bc6a -r a56b4e59bfd1 src/Tools/Argo/argo_proof.ML
--- a/src/Tools/Argo/argo_proof.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/Argo/argo_proof.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -52,7 +52,7 @@
 
   (* equalities and orders *)
   val eq_proof_id: proof_id * proof_id -> bool
-  val proof_id_ord: proof_id * proof_id -> order
+  val proof_id_ord: proof_id ord
 
   (* conversion constructors *)
   val keep_conv: conv
diff -r eecade21bc6a -r a56b4e59bfd1 src/Tools/Argo/argo_term.ML
--- a/src/Tools/Argo/argo_term.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/Argo/argo_term.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -17,7 +17,7 @@
   val expr_of: term -> Argo_Expr.expr
   val type_of: term -> Argo_Expr.typ
   val eq_term: term * term -> bool
-  val term_ord: term * term -> order
+  val term_ord: term ord
 
   (* context *)
   type context
diff -r eecade21bc6a -r a56b4e59bfd1 src/Tools/float.ML
--- a/src/Tools/float.ML	Tue Aug 20 15:42:23 2019 +0200
+++ b/src/Tools/float.ML	Tue Aug 20 20:23:21 2019 +0200
@@ -9,7 +9,7 @@
   type float = int * int
   val zero: float
   val eq: float * float -> bool
-  val ord: float * float -> order
+  val ord: float ord
   val sign: float -> order
   val min: float -> float -> float
   val max: float -> float -> float