equal
deleted
inserted
replaced
151 (bn_fun_strs ~~ bn_fun_strs') |
151 (bn_fun_strs ~~ bn_fun_strs') |
152 |
152 |
153 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
153 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
154 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
154 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
155 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
155 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
156 |
|
157 val _ = tracing ("raw_dt info:\n" ^ @{make_string} raw_dts) |
|
158 |
156 |
159 val (raw_dt_full_names, thy1) = |
157 val (raw_dt_full_names, thy1) = |
160 Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy |
158 Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy |
161 |
159 |
162 val lthy1 = Named_Target.theory_init thy1 |
160 val lthy1 = Named_Target.theory_init thy1 |