Renamed sum_case to basic_sum_case.
authorberghofe
Wed Aug 18 16:19:53 1999 +0200 (1999-08-18)
changeset 7257745cfc8871e2
parent 7256 0a69baf28961
child 7258 b228e54a02c5
Renamed sum_case to basic_sum_case.
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 18 16:19:01 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 18 16:19:53 1999 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4            let
     1.5              val n2 = n div 2;
     1.6              val Type (_, [T1, T2]) = T;
     1.7 -            val sum_case = Const ("sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
     1.8 +            val sum_case = Const ("basic_sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
     1.9            in
    1.10              if i <= n2 then
    1.11                sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Aug 18 16:19:01 1999 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 18 16:19:53 1999 +0200
     2.3 @@ -463,7 +463,7 @@
     2.4        | mk_ind_pred T Ps =
     2.5           let val n = (length Ps) div 2;
     2.6               val Type (_, [T1, T2]) = T
     2.7 -         in Const ("sum_case",
     2.8 +         in Const ("basic_sum_case",
     2.9             [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
    2.10               mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
    2.11           end;