diff -r 59b41ba431b5 -r cfe605c54e50 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Feb 10 14:12:04 2010 +0100
@@ -184,7 +184,7 @@
     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
@@ -561,7 +561,7 @@
          (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}));