--- a/src/HOL/Hoare/hoare.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Hoare/hoare.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -65,7 +65,7 @@
 fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
                       in Collect_const t $ trm end;
 
-fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
 
 (** Makes "Mset <= t" **)
 fun Mset_incl t = let val MsetT = fastype_of t