src/Pure/raw_simplifier.ML

      {mk: Proof.context -> thm -> thm list,
       mk_cong: Proof.context -> thm -> thm,
       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}
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
   val prems_of: Proof.context -> thm list

   val mksimps: Proof.context -> thm -> thm list
   val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context
   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
   val add_prems: thm list -> Proof.context -> Proof.context
   val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->

      {mk: Proof.context -> thm -> thm list,
       mk_cong: Proof.context -> thm -> thm,
       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};
 
 fun internal_ss (Simpset (_, ss2)) = ss2;