equal
deleted
inserted
replaced
434 |
434 |
435 fun normalize thy naming program ((vs0, (vs, ty)), t) deps = |
435 fun normalize thy naming program ((vs0, (vs, ty)), t) deps = |
436 let |
436 let |
437 fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty) |
437 fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty) |
438 | t => t); |
438 | t => t); |
439 val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy); |
439 val resubst_triv_consts = subst_const (Code.resubst_alias thy); |
440 val ty' = typ_of_itype program vs0 ty; |
440 val ty' = typ_of_itype program vs0 ty; |
441 fun type_infer t = |
441 fun type_infer t = |
442 singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I |
442 singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I |
443 (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0) |
443 (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0) |
444 (TypeInfer.constrain ty' t); |
444 (TypeInfer.constrain ty' t); |
457 end; |
457 end; |
458 |
458 |
459 (* evaluation oracle *) |
459 (* evaluation oracle *) |
460 |
460 |
461 fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy)) |
461 fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy)) |
462 (Code_Unit.triv_classes thy); |
462 (Code.triv_classes thy); |
463 |
463 |
464 fun mk_equals thy lhs raw_rhs = |
464 fun mk_equals thy lhs raw_rhs = |
465 let |
465 let |
466 val ty = Thm.typ_of (Thm.ctyp_of_term lhs); |
466 val ty = Thm.typ_of (Thm.ctyp_of_term lhs); |
467 val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT)); |
467 val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT)); |