--- 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;
--- 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;
--- 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
--- 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
--- 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
--- 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 ->
--- 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;
--- 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
--- 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,
--- 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
--- 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
--- 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
--- 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 =
--- 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
--- 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
--- 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
--- 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
--- 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;
--- 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
--- 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
--- 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};
--- 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
--- 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;
--- 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;
--- 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
--- 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
--- 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 *)
--- 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
--- 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
--- 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