equal
deleted
inserted
replaced
267 in |
267 in |
268 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
268 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
269 end |
269 end |
270 *} |
270 *} |
271 |
271 |
272 ML {* val cheat_alpha_eqvt = ref true *} |
272 (* These 2 are critical, we don't know how to do it in term5 *) |
273 ML {* val cheat_fv_eqvt = ref true *} (* Needed for non-rec *) |
|
274 ML {* val cheat_fv_rsp = ref true *} |
273 ML {* val cheat_fv_rsp = ref true *} |
275 ML {* val cheat_const_rsp = ref true *} |
274 ML {* val cheat_const_rsp = ref true *} (* For alpha_bn 0 and alpha_bn_rsp *) |
276 |
275 |
277 ML {* unsuffix "sdf" "aasdf" *} |
276 (* Fixes for these 2 are known *) |
|
277 ML {* val cheat_fv_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
|
278 ML {* val cheat_alpha_eqvt = ref true *} (* The tactic works, building the goal needs fixing *) |
278 |
279 |
279 ML {* |
280 ML {* |
280 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
281 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
281 let |
282 let |
282 val thy = ProofContext.theory_of lthy |
283 val thy = ProofContext.theory_of lthy |
488 map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs |
489 map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs |
489 |
490 |
490 fun prep_bn env bn_str = |
491 fun prep_bn env bn_str = |
491 case (Syntax.read_term lthy bn_str) of |
492 case (Syntax.read_term lthy bn_str) of |
492 Free (x, _) => (NONE, env_lookup env x) |
493 Free (x, _) => (NONE, env_lookup env x) |
493 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), false), env_lookup env x) |
494 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x) |
494 | _ => error (bn_str ^ " not allowed as binding specification."); |
495 | _ => error (bn_str ^ " not allowed as binding specification."); |
495 |
496 |
496 fun prep_typ env (i, opt_name) = |
497 fun prep_typ env (i, opt_name) = |
497 case opt_name of |
498 case opt_name of |
498 NONE => [] |
499 NONE => [] |