equal
deleted
inserted
replaced
712 |
712 |
713 |
713 |
714 |
714 |
715 (** check/uncheck **) |
715 (** check/uncheck **) |
716 |
716 |
717 fun check_typs ctxt = Syntax.typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt); |
717 fun check_typs ctxt = |
718 fun check_terms ctxt = Syntax.term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt); |
718 Syntax.apply_typ_check ctxt #> Term_Sharing.typs (Proof_Context.theory_of ctxt); |
|
719 |
|
720 fun check_terms ctxt = |
|
721 Syntax.apply_term_check ctxt #> Term_Sharing.terms (Proof_Context.theory_of ctxt); |
|
722 |
719 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt; |
723 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt; |
720 |
724 |
721 val uncheck_typs = Syntax.typ_uncheck; |
725 val uncheck_typs = Syntax.apply_typ_uncheck; |
722 val uncheck_terms = Syntax.term_uncheck; |
726 val uncheck_terms = Syntax.apply_term_uncheck; |
723 |
727 |
724 |
728 |
725 |
729 |
726 (** install operations **) |
730 (** install operations **) |
727 |
731 |