src/HOL/Orderings.thy

            | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
       | dec (Const (@{const_name "op ="},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "=", t2)
           else NONE
-      | dec (Const (@{const_name less_eq},  _) $ t1 $ t2) =
+      | dec (Const (@{const_name Orderings.less_eq},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<=", t2)
           else NONE
-      | dec (Const (@{const_name less},  _) $ t1 $ t2) =
+      | dec (Const (@{const_name Orderings.less},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<", t2)
           else NONE
       | dec _ = NONE;
   in dec t end;