equal
deleted
inserted
replaced
137 *} |
137 *} |
138 |
138 |
139 ML {* |
139 ML {* |
140 fun print_dts (dts, (funs, feqs)) lthy = |
140 fun print_dts (dts, (funs, feqs)) lthy = |
141 let |
141 let |
142 val _ = warning (implode (separate "\n" (map single_dt dts))) |
142 val _ = warning (implode (separate "\n" (map single_dt dts))) |
143 val _ = warning (implode (separate "\n" (map single_fun_fix funs))) |
143 val _ = warning (implode (separate "\n" (map single_fun_fix funs))) |
144 val _ = warning (implode (separate "\n" (map single_fun_eq feqs))) |
144 val _ = warning (implode (separate "\n" (map single_fun_eq feqs))) |
145 val _ = warning (implode (separate "\n" (map fv_dt dts))) |
145 val _ = warning (implode (separate "\n" (map fv_dt dts))) |
146 in |
146 in |
147 () |
147 lthy |
148 end |
148 end |
149 *} |
149 *} |
150 |
150 |
151 ML {* |
151 ML {* |
152 parser; |
152 parser; |
172 thy' |
172 thy' |
173 end |
173 end |
174 *} |
174 *} |
175 |
175 |
176 ML {* |
176 ML {* |
177 fun fn_defn [] [] thy = thy |
177 fun fn_defn [] [] lthy = lthy |
178 | fn_defn funs feqs thy = |
178 | fn_defn funs feqs lthy = |
179 let |
179 Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
180 val lthy = Theory_Target.init NONE thy |
|
181 val lthy = Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
|
182 val thy' = Local_Theory.exit_global ctxt |
|
183 in |
|
184 thy' |
|
185 end |
|
186 *} |
180 *} |
187 |
181 |
188 |
182 |
189 ML {* |
183 ML {* |
190 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
184 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
191 dt_defn (map transp_dt dts) thy |
185 dt_defn (map transp_dt dts) thy |
|
186 |> Theory_Target.init NONE |
192 |> fn_defn funs feqs |
187 |> fn_defn funs feqs |
193 |> Theory_Target.init NONE |
|
194 |> print_dts (dts, (funs, feqs)) |
188 |> print_dts (dts, (funs, feqs)) |
195 |> Local_Theory.exit_global |
189 |> Local_Theory.exit_global |
196 *} |
190 *} |
197 |
191 |
198 (* Command Keyword *) |
192 (* Command Keyword *) |