src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

 fun bunches_of_proof_methods ctxt smt_proofs needs_full_types desperate_lam_trans =
   let
     val misc_methodss =
       [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
         Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method,
-        Argo_Method]]
+        Argo_Method, Order_Method]]
 
     val metis_methodss =
       [Metis_Method (SOME full_typesN, NONE) ::
        Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) ::
        (if needs_full_types then