1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 17:26:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 17:26:05 2012 +0200
     1.3 @@ -32,18 +32,6 @@
     1.4  open BNF_FP_Util
     1.5  open BNF_FP_Sugar_Tactics
     1.6  
     1.7 -val caseN = "case";
     1.8 -val coinductsN = "coinducts";
     1.9 -val coitersN = "coiters";
    1.10 -val corecsN = "corecs";
    1.11 -val disc_coitersN = "disc_coiters";
    1.12 -val disc_corecsN = "disc_corecs";
    1.13 -val inductsN = "inducts";
    1.14 -val itersN = "iters";
    1.15 -val recsN = "recs";
    1.16 -val sel_coitersN = "sel_coiters";
    1.17 -val sel_corecsN = "sel_corecs";
    1.18 -
    1.19  val simp_attrs = @{attributes [simp]};
    1.20  
    1.21  fun split_list11 xs =

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 17:26:05 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 17:26:05 2012 +0200
     2.3 @@ -15,11 +15,16 @@
     2.4    val behN: string
     2.5    val bisN: string
     2.6    val carTN: string
     2.7 +  val caseN: string
     2.8    val coN: string
     2.9    val coinductN: string
    2.10 +  val coinductsN: string
    2.11    val coiterN: string
    2.12 -  val unf_coiter_uniqueN: string
    2.13 +  val coitersN: string
    2.14    val corecN: string
    2.15 +  val corecsN: string
    2.16 +  val disc_coitersN: string
    2.17 +  val disc_corecsN: string
    2.18    val exhaustN: string
    2.19    val fldN: string
    2.20    val fld_exhaustN: string
    2.21 @@ -27,6 +32,7 @@
    2.22    val fld_inductN: string
    2.23    val fld_injectN: string
    2.24    val fld_iterN: string
    2.25 +  val fld_iter_uniqueN: string
    2.26    val fld_itersN: string
    2.27    val fld_recN: string
    2.28    val fld_recsN: string
    2.29 @@ -36,10 +42,11 @@
    2.30    val hsetN: string
    2.31    val hset_recN: string
    2.32    val inductN: string
    2.33 +  val inductsN: string
    2.34    val injectN: string
    2.35    val isNodeN: string
    2.36    val iterN: string
    2.37 -  val fld_iter_uniqueN: string
    2.38 +  val itersN: string
    2.39    val lsbisN: string
    2.40    val map_simpsN: string
    2.41    val map_uniqueN: string
    2.42 @@ -49,9 +56,12 @@
    2.43    val pred_coinductN: string
    2.44    val pred_coinduct_uptoN: string
    2.45    val recN: string
    2.46 +  val recsN: string
    2.47    val rel_coinductN: string
    2.48    val rel_coinduct_uptoN: string
    2.49    val rvN: string
    2.50 +  val sel_coitersN: string
    2.51 +  val sel_corecsN: string
    2.52    val set_inclN: string
    2.53    val set_set_inclN: string
    2.54    val strTN: string
    2.55 @@ -62,6 +72,7 @@
    2.56    val unf_coinductN: string
    2.57    val unf_coinduct_uptoN: string
    2.58    val unf_coiterN: string
    2.59 +  val unf_coiter_uniqueN: string
    2.60    val unf_coitersN: string
    2.61    val unf_corecN: string
    2.62    val unf_corecsN: string
    2.63 @@ -214,6 +225,18 @@
    2.64  val set_inclN = "set_incl"
    2.65  val set_set_inclN = "set_set_incl"
    2.66  
    2.67 +val caseN = "case"
    2.68 +val coinductsN = "coinducts"
    2.69 +val coitersN = "coiters"
    2.70 +val corecsN = "corecs"
    2.71 +val disc_coitersN = "disc_coiters"
    2.72 +val disc_corecsN = "disc_corecs"
    2.73 +val inductsN = "inducts"
    2.74 +val itersN = "iters"
    2.75 +val recsN = "recs"
    2.76 +val sel_coitersN = "sel_coiters"
    2.77 +val sel_corecsN = "sel_corecs"
    2.78 +
    2.79  val mk_common_name = space_implode "_" o map Binding.name_of;
    2.80  
    2.81  fun mk_predT T = T --> HOLogic.boolT;