changeset 7257 | 745cfc8871e2 |
parent 7152 | 44d46a112127 |
child 7293 | 959e060f4a2f |
--- 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;