# HG changeset patch
# User lcp
# Date 794579376 -3600
# Node ID b7ab0425332696ba7c364d44e732a8bfaf71c341
# Parent  c1e2004d07bd15bd32854887f4be790218a05f5e
Got rid of exvarU and constU by
including ExVar and Const in various datatype universes.

diff -r c1e2004d07bd -r b7ab04253326 src/ZF/Coind/Language.thy
--- 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
-
-
-
-