--- a/src/ZF/Coind/Values.thy Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/Coind/Values.thy Sun Oct 07 21:19:31 2007 +0200
@@ -33,8 +33,8 @@
primrec "ve_app(ve_mk(m), a) = map_app(m,a)"
-constdefs
- ve_emp :: i
+definition
+ ve_emp :: i where
"ve_emp == ve_mk(map_emp)"