1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 12:07:15 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 12:51:17 2012 +0200
     1.3 @@ -489,9 +489,6 @@
     1.4                else
     1.5                  [x];
     1.6  
     1.7 -            fun repair_rec_call (x as Free (_, T)) =
     1.8 -              (case find_index (curry (op =) T) fpTs of ~1 => [x] | j => [x, nth hrecs j $ x]);
     1.9 -
    1.10              val gxsss = map (map (maps (repair_calls giters (K I) (K I) (K I)))) xsss;
    1.11              val hxsss =
    1.12                map (map (maps (repair_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
    1.13 @@ -524,7 +521,6 @@
    1.14      fun pour_more_sugar_on_gfps ((ctrss, coiters, corecs, vs, xsss, ctr_defss, coiter_defs,
    1.15          corec_defs), lthy) =
    1.16        let
    1.17 -(* NOTYET
    1.18          val gcoiters = map (lists_bmoc pgss) coiters;
    1.19          val hcorecs = map (lists_bmoc phss) corecs;
    1.20  
    1.21 @@ -541,12 +537,9 @@
    1.22                (case find_index (curry (op =) T) Cs of ~1 => cf | j => nth fcoiter_likes j $ cf);
    1.23  
    1.24              val cgsss = map (map (map (repair_call gcoiters))) cgsss;
    1.25 -            val chsss = map (map (map (repair_call hcorecs))) chsss;
    1.26  
    1.27              val goal_coiterss =
    1.28                map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;
    1.29 -            val goal_corecss =
    1.30 -              map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
    1.31  
    1.32              val coiter_tacss =
    1.33                map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
    1.34 @@ -554,20 +547,17 @@
    1.35            in
    1.36              (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.37                 goal_coiterss coiter_tacss,
    1.38 -             map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.39 -               goal_coiterss coiter_tacss (* TODO: should be corecs *))
    1.40 +             [])
    1.41            end;
    1.42  
    1.43          val notes =
    1.44 -          [(coitersN, coiter_thmss),
    1.45 -           (corecsN, corec_thmss)]
    1.46 +          [(coitersN, coiter_thmss)]
    1.47            |> maps (fn (thmN, thmss) =>
    1.48              map2 (fn b => fn thms =>
    1.49                  ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    1.50                bs thmss);
    1.51 -*)
    1.52        in
    1.53 -        lthy (* NOTYET |> Local_Theory.notes notes |> snd *)
    1.54 +        lthy |> Local_Theory.notes notes |> snd
    1.55        end;
    1.56  
    1.57      val lthy' = lthy