| changeset 34974 | 18b41bba42b5 |
| parent 32149 | ef59550a55d3 |
| child 35092 | cfe605c54e50 |
--- a/src/HOL/Hoare/hoare_tac.ML Thu Jan 28 11:48:43 2010 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Thu Jan 28 11:48:49 2010 +0100 @@ -58,7 +58,7 @@ let val T as Type ("fun",[t,_]) = fastype_of trm in Collect_const t $ trm end; -fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT); +fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT); fun Mset ctxt prop =