equal
deleted
inserted
replaced
274 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
274 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
275 end |
275 end |
276 *} |
276 *} |
277 |
277 |
278 (* These 2 are critical, we don't know how to do it in term5 *) |
278 (* These 2 are critical, we don't know how to do it in term5 *) |
279 ML {* val cheat_fv_rsp = ref true *} |
279 ML {* val cheat_fv_rsp = Unsynchronized.ref true *} |
280 ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
280 ML {* val cheat_const_rsp = Unsynchronized.ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
281 |
281 |
282 ML {* val cheat_equivp = ref true *} |
282 ML {* val cheat_equivp = Unsynchronized.ref true *} |
283 |
283 |
284 (* Fixes for these 2 are known *) |
284 (* Fixes for these 2 are known *) |
285 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
285 ML {* val cheat_fv_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *) |
286 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
286 ML {* val cheat_alpha_eqvt = Unsynchronized.ref true *} (* The tactic works, building the goal needs fixing *) |
287 |
287 |
288 |
288 |
289 ML {* |
289 ML {* |
290 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
290 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
291 let |
291 let |
520 SOME x => x |
520 SOME x => x |
521 | NONE => error ("cannot find " ^ x ^ " in the binding specification."); |
521 | NONE => error ("cannot find " ^ x ^ " in the binding specification."); |
522 *} |
522 *} |
523 |
523 |
524 ML {* |
524 ML {* |
525 val recursive = ref false |
525 val recursive = Unsynchronized.ref false |
526 *} |
526 *} |
527 |
527 |
528 ML {* |
528 ML {* |
529 fun prepare_binds dt_strs lthy = |
529 fun prepare_binds dt_strs lthy = |
530 let |
530 let |