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 |
518 SOME x => x |
518 SOME x => x |
519 | NONE => error ("cannot find " ^ x ^ " in the binding specification."); |
519 | NONE => error ("cannot find " ^ x ^ " in the binding specification."); |
520 *} |
520 *} |
521 |
521 |
522 ML {* |
522 ML {* |
523 val recursive = ref false |
523 val recursive = Unsynchronized.ref false |
524 *} |
524 *} |
525 |
525 |
526 ML {* |
526 ML {* |
527 fun prepare_binds dt_strs lthy = |
527 fun prepare_binds dt_strs lthy = |
528 let |
528 let |