src/HOL/Codatatype/Tools/bnf_util.ML
changeset 49255 2ecc533d6697
parent 49228 e43910ccee74
child 49282 c057e1b39f16
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 10 17:32:39 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 10 17:35:53 2012 +0200
     1.3 @@ -62,7 +62,6 @@
     1.4    val mk_relT: typ * typ -> typ
     1.5    val dest_relT: typ -> typ * typ
     1.6    val mk_sumT: typ * typ -> typ
     1.7 -  val mk_sumTN: typ list -> typ
     1.8  
     1.9    val ctwo: term
    1.10    val fst_const: typ -> term
    1.11 @@ -304,7 +303,6 @@
    1.12  val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
    1.13  val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
    1.14  fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]);
    1.15 -fun mk_sumTN Ts = Library.foldr1 mk_sumT Ts;
    1.16  fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT;
    1.17  
    1.18