equal
deleted
inserted
replaced
153 fun find [] _ = error ("cannot find element") |
153 fun find [] _ = error ("cannot find element") |
154 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
154 | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y |
155 *} |
155 *} |
156 |
156 |
157 ML {* |
157 ML {* |
158 fun prep_bn dt_names dts eqs lthy = |
158 fun prep_bn dt_names dts eqs = |
159 let |
159 let |
160 fun aux eq = |
160 fun aux eq = |
161 let |
161 let |
162 val (lhs, rhs) = eq |
162 val (lhs, rhs) = eq |
163 |> strip_qnt_body "all" |
163 |> strip_qnt_body "all" |
239 |
239 |
240 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
240 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
241 |
241 |
242 val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds |
242 val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds |
243 |
243 |
244 val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) lthy |
244 val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) |
245 |
245 |
246 val _ = tracing (cat_lines (map PolyML.makestring raw_bns)) |
246 val _ = tracing (cat_lines (map PolyML.makestring raw_bns)) |
247 in |
247 in |
248 lthy |
248 lthy |
249 |> add_datatype_wrapper raw_dt_names raw_dts |
249 |> add_datatype_wrapper raw_dt_names raw_dts |