diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Coind/Values.thy	Wed Jan 13 11:57:09 1999 +0100
@@ -10,11 +10,12 @@
 
 consts
   Val, ValEnv, Val_ValEnv  :: i
-codatatype <= "quniv(Const Un ExVar Un Exp)"
-    "Val" = v_const("c:Const")
-          | v_clos("x:ExVar","e:Exp","ve:ValEnv")
+
+codatatype
+    "Val" = v_const ("c:Const")
+          | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
   and
-    "ValEnv" = ve_mk("m:PMap(ExVar,Val)")
+    "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
   monos      "[map_mono]"
   type_intrs "[A_into_univ, mapQU]"