# HG changeset patch
# User berghofe
# Date 935082117 -7200
# Node ID 5a50de9141b5e2947a3f3f169f8acde63e371b68
# Parent  959e060f4a2fcdfdb269ef93b9fa16a0d5e6aa62
sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.

diff -r 959e060f4a2f -r 5a50de9141b5 src/HOLCF/Up1.ML
--- 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 =>
         [