243 |
243 |
244 fun add_recursor thy = |
244 fun add_recursor thy = |
245 if need_recursor then |
245 if need_recursor then |
246 thy |> Theory.add_consts_i |
246 thy |> Theory.add_consts_i |
247 [(recursor_base_name, recursor_typ, NoSyn)] |
247 [(recursor_base_name, recursor_typ, NoSyn)] |
248 |> (#1 o PureThy.add_defs_i [Thm.no_attributes recursor_def]) |
248 |> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def]) |
249 else thy; |
249 else thy; |
250 |
250 |
251 val (thy0, con_defs) = thy_path |
251 val (thy0, con_defs) = thy_path |
252 |> Theory.add_consts_i |
252 |> Theory.add_consts_i |
253 ((case_base_name, case_typ, NoSyn) :: |
253 ((case_base_name, case_typ, NoSyn) :: |
254 map #1 (flat con_ty_lists)) |
254 map #1 (flat con_ty_lists)) |
255 |> PureThy.add_defs_i |
255 |> PureThy.add_defs_i false |
256 (map Thm.no_attributes |
256 (map Thm.no_attributes |
257 (case_def :: |
257 (case_def :: |
258 flat (ListPair.map mk_con_defs |
258 flat (ListPair.map mk_con_defs |
259 (1 upto npart, con_ty_lists)))) |
259 (1 upto npart, con_ty_lists)))) |
260 |>> add_recursor |
260 |>> add_recursor |