diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Values.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 (* Values, values environments and associated operators *)
 
 consts
-  Val, ValEnv, Val_ValEnv  :: "i"
+  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")
@@ -19,10 +19,10 @@
   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"
+  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