src/HOL/Codatatype/Tools/bnf_fp_util.ML
changeset 49330 276ff43ee0b1
parent 49327 541d818d2ff3
child 49335 096967bf3940
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 11:47:51 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 12:06:03 2012 +0200
     1.3 @@ -83,6 +83,10 @@
     1.4    val split_conj_thm: thm -> thm list
     1.5    val split_conj_prems: int -> thm -> thm
     1.6  
     1.7 +  val retype_free: typ -> term -> term
     1.8 +
     1.9 +  val mk_predT: typ -> typ;
    1.10 +
    1.11    val mk_sumTN: typ list -> typ
    1.12    val mk_sumTN_balanced: typ list -> typ
    1.13  
    1.14 @@ -211,6 +215,10 @@
    1.15  
    1.16  val mk_bundle_name = space_implode "_" o map Binding.name_of;
    1.17  
    1.18 +fun mk_predT T = T --> HOLogic.boolT;
    1.19 +
    1.20 +fun retype_free T (Free (s, _)) = Free (s, T);
    1.21 +
    1.22  fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
    1.23  
    1.24  fun dest_sumTN 1 T = [T]