diff -r 6a9dc67d48f5 -r 2c8a8be36c94 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Mon Dec 28 16:53:24 1998 +0100
+++ b/src/ZF/Coind/Values.thy	Mon Dec 28 16:54:01 1998 +0100
@@ -19,19 +19,20 @@
   type_intrs "[A_into_univ, mapQU]"
 
 consts
-  ve_emp :: i
   ve_owr :: [i,i,i] => i
   ve_dom :: i=>i
   ve_app :: [i,i] => i
-defs
-  ve_emp_def "ve_emp == ve_mk(map_emp)"
-  ve_owr_def
-    "ve_owr(ve,x,v) ==   
-    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m. map_owr(m,x,v),ve))"
-  ve_dom_def
-    "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m. domain(m),ve)"
-  ve_app_def
-    "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m. map_app(m,a),ve)"
+
+
+primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"
+
+primrec "ve_dom(ve_mk(m)) = domain(m)"
+
+primrec "ve_app(ve_mk(m), a) = map_app(m,a)"
+
+constdefs
+  ve_emp :: i
+   "ve_emp == ve_mk(map_emp)"
 
 end