src/HOL/Tools/inductive.ML

       handle THM _ => thm RS @{thm le_boolD}
   in
     case concl_of thm of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
-    | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) =>
+    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
       dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
     | _ => thm
   end handle THM _ =>
     error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);

       (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
          (make_bool_args HOLogic.mk_not I bs i)
          (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
 
     val ind_concl = HOLogic.mk_Trueprop
-      (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred));
+      (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
 
     val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
 
     val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl
       (fn {prems, ...} => EVERY