# HG changeset patch
# User berghofe
# Date 934985474 -7200
# Node ID fc7f95f293da016245eb4177ad127ea5d2fcd63c
# Parent  a494a78fea3927b6ec3a31e77a46c44a58723bee
Renamed sum_case to basic_sum_case and removed translations for sum_case
to avoid conflicts with the constant sum_case introduced in Datatype.thy.

diff -r a494a78fea39 -r fc7f95f293da src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Wed Aug 18 16:05:27 1999 +0200
+++ b/src/HOL/Sum.ML	Wed Aug 18 16:11:14 1999 +0200
@@ -116,11 +116,11 @@
 
 (** sum_case -- the selection operator for sums **)
 
-Goalw [sum_case_def] "sum_case f g (Inl x) = f(x)";
+Goalw [sum_case_def] "basic_sum_case f g (Inl x) = f(x)";
 by (Blast_tac 1);
 qed "sum_case_Inl";
 
-Goalw [sum_case_def] "sum_case f g (Inr x) = g(x)";
+Goalw [sum_case_def] "basic_sum_case f g (Inr x) = g(x)";
 by (Blast_tac 1);
 qed "sum_case_Inr";
 
@@ -143,31 +143,31 @@
 by (ALLGOALS (hyp_subst_tac THEN' (resolve_tac prems)));
 qed "sum_induct";
 
-Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
+Goal "basic_sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
             etac ssubst, rtac sum_case_Inl,
             etac ssubst, rtac sum_case_Inr]);
 qed "surjective_sum";
 
-Goal "R(sum_case f g s) = \
+Goal "R(basic_sum_case f g s) = \
 \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
 by (res_inst_tac [("s","s")] sumE 1);
 by Auto_tac;
 qed "split_sum_case";
 
-Goal "P (sum_case f g s) = \
+Goal "P (basic_sum_case f g s) = \
 \     (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
 by (stac split_sum_case 1);
 by (Blast_tac 1);
 qed "split_sum_case_asm";
 
 (*Prevents simplification of f and g: much faster*)
-Goal "s=t ==> sum_case f g s = sum_case f g t";
+Goal "s=t ==> basic_sum_case f g s = basic_sum_case f g t";
 by (etac arg_cong 1);
 qed "sum_case_weak_cong";
 
 val [p1,p2] = Goal
-  "[| sum_case f1 f2 = sum_case g1 g2;  \
+  "[| basic_sum_case f1 f2 = basic_sum_case g1 g2;  \
 \     [| f1 = g1; f2 = g2 |] ==> P |] \
 \  ==> P";
 by (rtac p2 1);
diff -r a494a78fea39 -r fc7f95f293da src/HOL/Sum.thy
--- a/src/HOL/Sum.thy	Wed Aug 18 16:05:27 1999 +0200
+++ b/src/HOL/Sum.thy	Wed Aug 18 16:11:14 1999 +0200
@@ -27,23 +27,20 @@
 (* abstract constants and syntax *)
 
 consts
-  Inl           :: "'a => 'a + 'b"
-  Inr           :: "'b => 'a + 'b"
-  sum_case      :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
+  Inl            :: "'a => 'a + 'b"
+  Inr            :: "'b => 'a + 'b"
+  basic_sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c"
 
   (*disjoint sum for sets; the operator + is overloaded with wrong type!*)
   Plus          :: "['a set, 'b set] => ('a + 'b) set"        (infixr 65)
   Part          :: ['a set, 'b => 'a] => 'a set
 
-translations
-  "case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
-
 local
 
 defs
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
-  sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
+  sum_case_def  "basic_sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
                                       & (!y. p=Inr(y) --> z=g(y))"
 
   sum_def       "A Plus B == (Inl``A) Un (Inr``B)"