src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
changeset 49213 975ccb0130cb
parent 49212 ca59649170b0
child 49214 2a3cb4c71b87
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4  open BNF_FP_Sugar_Tactics
     1.5  
     1.6  val caseN = "case";
     1.7 -val coitersN = "iters";
     1.8 -val corecsN = "recs";
     1.9 +val coitersN = "coiters";
    1.10 +val corecsN = "corecs";
    1.11  val itersN = "iters";
    1.12  val recsN = "recs";
    1.13  
    1.14 @@ -480,9 +480,14 @@
    1.15                map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;
    1.16              val goal_corecss =
    1.17                map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
    1.18 +
    1.19 +            val coiter_tacss =
    1.20 +              map3 (map oo mk_coiter_like_tac coiter_defs) fp_iter_thms pre_map_defs ctr_defss;
    1.21            in
    1.22 -            (map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss,
    1.23 -             map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss (*### goal_corecss*))
    1.24 +            (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.25 +               goal_coiterss coiter_tacss,
    1.26 +             map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.27 +               goal_coiterss coiter_tacss (* TODO: should be corecs *))
    1.28            end;
    1.29  
    1.30          val notes =