# HG changeset patch
# User wenzelm
# Date 1566291665 -7200
# Node ID 57df8a85317a5160e15a19d9306fa56261ef64ca
# Parent  17909568216ef9460accbb8ff8f22b380a424efe
clarified signature;

diff -r 17909568216e -r 57df8a85317a src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/groebner.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/General/heap.ML
--- a/src/Pure/General/heap.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/General/heap.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/General/name_space.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/General/rat.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/General/table.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/context.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/defs.ML
--- a/src/Pure/defs.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/defs.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/library.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/more_thm.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Aug 20 11:01:05 2019 +0200
@@ -51,8 +51,8 @@
     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: pthm 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
diff -r 17909568216e -r 57df8a85317a src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/simplifier.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/term_ord.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/thm.ML	Tue Aug 20 11:01:05 2019 +0200
@@ -371,7 +371,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;
diff -r 17909568216e -r 57df8a85317a src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/thm_name.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/variable.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Tools/Argo/argo_expr.ML
--- a/src/Tools/Argo/argo_expr.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Tools/Argo/argo_expr.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Tools/Argo/argo_proof.ML
--- a/src/Tools/Argo/argo_proof.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Tools/Argo/argo_proof.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Tools/Argo/argo_term.ML
--- a/src/Tools/Argo/argo_term.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Tools/Argo/argo_term.ML	Tue Aug 20 11:01:05 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 17909568216e -r 57df8a85317a src/Tools/float.ML
--- a/src/Tools/float.ML	Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Tools/float.ML	Tue Aug 20 11:01:05 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