equal
deleted
inserted
replaced
133 Symtab.map_default (constr, []) (cons dtname_info)) |
133 Symtab.map_default (constr, []) (cons dtname_info)) |
134 (maps (fn (dtname, info as {descr, index, ...}) => |
134 (maps (fn (dtname, info as {descr, index, ...}) => |
135 map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos), |
135 map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos), |
136 cases = cases |> fold Symtab.update |
136 cases = cases |> fold Symtab.update |
137 (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #> |
137 (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #> |
138 fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos; |
138 fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos; |
139 |
139 |
140 |
140 |
141 (* complex queries *) |
141 (* complex queries *) |
142 |
142 |
143 fun the_spec thy dtco = |
143 fun the_spec thy dtco = |