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