src/HOL/Tools/Function/termination.ML
changeset 35092 cfe605c54e50
parent 34974 18b41bba42b5
child 35402 115a5a95710a
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -203,10 +203,10 @@
     1.4               HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
     1.5                 $ (m2 $ r) $ (m1 $ l)))))) tac
     1.6    in
     1.7 -    case try @{const_name Algebras.less} of
     1.8 +    case try @{const_name Orderings.less} of
     1.9         Solved thm => Less thm
    1.10       | Stuck thm =>
    1.11 -       (case try @{const_name Algebras.less_eq} of
    1.12 +       (case try @{const_name Orderings.less_eq} of
    1.13            Solved thm2 => LessEq (thm2, thm)
    1.14          | Stuck thm2 =>
    1.15            if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]