107 fun replace_term trm_ss ty_ss trm = |
107 fun replace_term trm_ss ty_ss trm = |
108 trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) |
108 trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) |
109 *} |
109 *} |
110 |
110 |
111 ML {* |
111 ML {* |
112 fun rawify_dts dt_names dts dts_env = |
112 fun rawify_dts dts dts_env = raw_dts dts_env dts |
113 let |
|
114 val raw_dts = raw_dts dts_env dts |
|
115 val raw_dt_names = add_raws dt_names |
|
116 in |
|
117 (raw_dt_names, raw_dts) |
|
118 end |
|
119 *} |
113 *} |
120 |
114 |
121 ML {* |
115 ML {* |
122 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = |
116 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = |
123 let |
117 let |
166 val bn_fun_strs' = add_raws bn_fun_strs |
160 val bn_fun_strs' = add_raws bn_fun_strs |
167 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
161 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
168 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
162 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
169 (bn_fun_strs ~~ bn_fun_strs') |
163 (bn_fun_strs ~~ bn_fun_strs') |
170 |
164 |
171 val (raw_full_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
165 val raw_dts = rawify_dts dts dts_env |
172 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
166 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
173 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
167 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses |
174 |
168 |
175 val (raw_full_dt_names', thy1) = |
169 val (raw_full_dt_names', thy1) = |
176 Datatype.add_datatype Datatype.default_config raw_full_dt_names raw_dts thy |
170 Datatype.add_datatype Datatype.default_config raw_dts thy |
177 |
171 |
178 val lthy1 = Named_Target.theory_init thy1 |
172 val lthy1 = Named_Target.theory_init thy1 |
179 |
173 |
180 val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' |
174 val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' |
181 val {descr, sorts, ...} = hd dtinfos |
175 val {descr, sorts, ...} = hd dtinfos |