--- a/src/HOL/Tools/Function/lexicographic_order.ML Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Wed Feb 10 14:12:04 2010 +0100
@@ -80,10 +80,10 @@
let
val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
in
- case try_proof (goals @{const_name Algebras.less}) solve_tac of
+ case try_proof (goals @{const_name Orderings.less}) solve_tac of
Solved thm => Less thm
| Stuck thm =>
- (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of
+ (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2