src/ZF/Coind/Values.thy
changeset 6117 f9aad8ccd590
parent 6112 5e4871c5136b
child 11318 6536fb8c9fc6
--- a/src/ZF/Coind/Values.thy	Wed Jan 13 12:44:33 1999 +0100
+++ b/src/ZF/Coind/Values.thy	Wed Jan 13 15:14:47 1999 +0100
@@ -16,8 +16,8 @@
           | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
   and
     "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
-  monos      "[map_mono]"
-  type_intrs "[A_into_univ, mapQU]"
+  monos       map_mono
+  type_intrs  A_into_univ, mapQU
 
 consts
   ve_owr :: [i,i,i] => i