--- a/src/HOLCF/Up1.ML Thu Aug 19 19:00:42 1999 +0200
+++ b/src/HOLCF/Up1.ML Thu Aug 19 19:01:57 1999 +0200
@@ -6,9 +6,6 @@
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 =>
[