# HG changeset patch
# User paulson
# Date 859987844 -7200
# Node ID b1e7e2179597ee9f7a1969be66dcf4a0326d0e37
# Parent  5f0599e154484aa5953d9cdf9270ea208df8a733
Datatype declarations now require theory Datatype--NOT in quotes

diff -r 5f0599e15448 -r b1e7e2179597 src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Wed Apr 02 15:29:48 1997 +0200
+++ b/src/ZF/Coind/Language.thy	Wed Apr 02 15:30:44 1997 +0200
@@ -4,7 +4,7 @@
     Copyright   1995  University of Cambridge
 *)
 
-Language ="Datatype" + QUniv +
+Language = Datatype + QUniv +
 
 consts
   Const :: i                    (* Abstract type of constants *)
diff -r 5f0599e15448 -r b1e7e2179597 src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Wed Apr 02 15:29:48 1997 +0200
+++ b/src/ZF/Resid/Redex.thy	Wed Apr 02 15:30:44 1997 +0200
@@ -5,7 +5,7 @@
     Logic Image: ZF
 *)
 
-Redex = Univ +
+Redex = Datatype +
 consts
   redexes     :: i