equal
deleted
inserted
replaced
176 val raw_distinct_thms = flat (map #distinct dtinfos) |
176 val raw_distinct_thms = flat (map #distinct dtinfos) |
177 val raw_induct_thm = #induct (hd dtinfos) |
177 val raw_induct_thm = #induct (hd dtinfos) |
178 val raw_induct_thms = #inducts (hd dtinfos) |
178 val raw_induct_thms = #inducts (hd dtinfos) |
179 val raw_exhaust_thms = map #exhaust dtinfos |
179 val raw_exhaust_thms = map #exhaust dtinfos |
180 val raw_size_trms = map HOLogic.size_const raw_tys |
180 val raw_size_trms = map HOLogic.size_const raw_tys |
181 val raw_size_thms = Size.size_thms (Proof_Context.theory_of lthy1) (hd raw_full_dt_names') |
181 val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd) |
182 |> `(fn thms => (length thms) div 2) |
182 (BNF_LFP_Size.lookup_size lthy1 (hd raw_full_dt_names'))) |
183 |> uncurry drop |
|
184 |
183 |
185 val raw_result = RawDtInfo |
184 val raw_result = RawDtInfo |
186 {raw_dt_names = raw_full_dt_names', |
185 {raw_dt_names = raw_full_dt_names', |
187 raw_dts = raw_dts, |
186 raw_dts = raw_dts, |
188 raw_tys = raw_tys, |
187 raw_tys = raw_tys, |