# HG changeset patch
# User wenzelm
# Date 925483270 -7200
# Node ID da7b170fc8a783514d07a857b6caefa4dac81ff3
# Parent  015c3813277a3aaedf1d2dc661439c7fb3aaa41a
patched sum_case;

diff -r 015c3813277a -r da7b170fc8a7 src/HOLCF/Up1.ML
--- a/src/HOLCF/Up1.ML	Thu Apr 29 22:45:19 1999 +0200
+++ b/src/HOLCF/Up1.ML	Fri Apr 30 16:41:10 1999 +0200
@@ -6,6 +6,9 @@
 
 open Up1;
 
+(*compatibility*)
+val [sum_case_Inl, sum_case_Inr] = sum.cases;
+
 qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
  (fn prems =>
         [
diff -r 015c3813277a -r da7b170fc8a7 src/HOLCF/Up1.thy
--- a/src/HOLCF/Up1.thy	Thu Apr 29 22:45:19 1999 +0200
+++ b/src/HOLCF/Up1.thy	Fri Apr 30 16:41:10 1999 +0200
@@ -8,7 +8,7 @@
 
 *)
 
-Up1 = Cfun3 + Sum + 
+Up1 = Cfun3 + Sum + Datatype +
 
 (* new type for lifting *)