# HG changeset patch
# User berghofe
# Date 934985993 -7200
# Node ID 745cfc8871e25f3fe87eac3c4dfea3403f3748f2
# Parent  0a69baf2896109c0295f53c630994b9790965093
Renamed sum_case to basic_sum_case.

diff -r 0a69baf28961 -r 745cfc8871e2 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 18 16:19:01 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 18 16:19:53 1999 +0200
@@ -124,7 +124,7 @@
           let
             val n2 = n div 2;
             val Type (_, [T1, T2]) = T;
-            val sum_case = Const ("sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
+            val sum_case = Const ("basic_sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
           in
             if i <= n2 then
               sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
diff -r 0a69baf28961 -r 745cfc8871e2 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Aug 18 16:19:01 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 18 16:19:53 1999 +0200
@@ -463,7 +463,7 @@
       | mk_ind_pred T Ps =
          let val n = (length Ps) div 2;
              val Type (_, [T1, T2]) = T
-         in Const ("sum_case",
+         in Const ("basic_sum_case",
            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
          end;