Got rid of exvarU and constU by
including ExVar and Const in various datatype universes.

--- a/src/ZF/Coind/Language.thy	Tue Mar 07 13:27:09 1995 +0100
+++ b/src/ZF/Coind/Language.thy	Tue Mar 07 13:29:36 1995 +0100
@@ -6,46 +6,23 @@
 
 Language ="Datatype" + QUniv +
 
-(* Abstract type of constants *)
+consts
+  Const :: "i"			(* Abstract type of constants *)
+  c_app :: "[i,i] => i"		(*Abstract constructor for fun application*)
 
-consts
-  Const :: "i"
 rules
-  constU "c:Const ==> c:univ(A)"
-  constNEE "c:Const ==> c ~= 0"
- 
-(* A function that captures how constant functions are applied to
-   constants *)
-  
-consts
-  c_app :: "[i,i] => i"
-rules
-  c_appI "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
+  constNEE  "c:Const ==> c ~= 0"
+  c_appI    "[| c1:Const; c2:Const |] ==> c_app(c1,c2):Const"
 
 
-(* Abstract type of variables *)
-
 consts
-  ExVar :: "i"
-rules
-  exvarU "x:ExVar ==> x:univ(A)"
-
-
-(* Datatype of expressions *)
-
-consts
-  Exp :: "i"
-datatype
-  "Exp" =
-    e_const("c:Const") |
-    e_var("x:ExVar") |
-    e_fn("x:ExVar","e:Exp") | 
-    e_fix("x1:ExVar","x2:ExVar","e:Exp") | 
-    e_app("e1:Exp","e2:Exp")
-  type_intrs "[constU,exvarU]"
+  Exp   :: "i"			(* Datatype of expressions *)
+  ExVar :: "i"			(* Abstract type of variables *)
+datatype <= "univ(Const Un ExVar)"
+  "Exp" = e_const("c:Const")
+        | e_var("x:ExVar")
+        | e_fn("x:ExVar","e:Exp")
+        | e_fix("x1:ExVar","x2:ExVar","e:Exp")
+        | e_app("e1:Exp","e2:Exp")
 
 end
-
-
-
-