--- a/src/HOLCF/Tools/domain/domain_library.ML Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML Fri May 08 16:19:51 2009 -0700
@@ -257,7 +257,7 @@
infix 0 ==; fun S == T = %%:"==" $ S $ T;
infix 1 ===; fun S === T = %%:"op =" $ S $ T;
infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
-infix 1 <<; fun S << T = %%: @{const_name Porder.sq_le} $ S $ T;
+infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T;
infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;