129 val infos = map mk_info (take nn_fp fp_sugars); |
129 val infos = map mk_info (take nn_fp fp_sugars); |
130 |
130 |
131 val all_notes = |
131 val all_notes = |
132 (case lfp_sugar_thms of |
132 (case lfp_sugar_thms of |
133 NONE => [] |
133 NONE => [] |
134 | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs), |
134 | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, _), (rec_thmss, _)) => |
135 (rec_thmss, rec_attrs)) => |
|
136 let |
135 let |
137 val common_notes = |
136 val common_notes = |
138 (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) |
137 (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) |
139 |> filter_out (null o #2) |
138 |> filter_out (null o #2) |
140 |> map (fn (thmN, thms, attrs) => |
139 |> map (fn (thmN, thms, attrs) => |
141 ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); |
140 ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); |
142 |
141 |
143 val notes = |
142 val notes = |
144 [(foldN, fold_thmss, fold_attrs), |
143 [(foldN, fold_thmss, []), |
145 (inductN, map single induct_thms, induct_attrs), |
144 (inductN, map single induct_thms, induct_attrs), |
146 (recN, rec_thmss, rec_attrs)] |
145 (recN, rec_thmss, [])] |
147 |> filter_out (null o #2) |
146 |> filter_out (null o #2) |
148 |> maps (fn (thmN, thmss, attrs) => |
147 |> maps (fn (thmN, thmss, attrs) => |
149 if forall null thmss then |
148 if forall null thmss then |
150 [] |
149 [] |
151 else |
150 else |