src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
changeset 50353 4a922800531d
parent 50352 538687a77075
child 50357 8ea4bad49ed5
     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 =