--- a/src/HOL/Tools/Function/termination.ML Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML Thu Jan 28 11:48:49 2010 +0100
@@ -203,10 +203,10 @@
HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
$ (m2 $ r) $ (m1 $ l)))))) tac
in
- case try @{const_name HOL.less} of
+ case try @{const_name Algebras.less} of
Solved thm => Less thm
| Stuck thm =>
- (case try @{const_name HOL.less_eq} of
+ (case try @{const_name Algebras.less_eq} of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]