equal
deleted
inserted
replaced
604 |
604 |
605 (* achieve plain syntax for locale predicates (without "PROP") *) |
605 (* achieve plain syntax for locale predicates (without "PROP") *) |
606 |
606 |
607 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => |
607 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => |
608 if length args = n then |
608 if length args = n then |
609 Syntax.const "_aprop" $ |
609 Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *) |
610 Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) |
610 Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) |
611 else raise Match); |
611 else raise Match); |
612 |
612 |
613 (* define one predicate including its intro rule and axioms |
613 (* define one predicate including its intro rule and axioms |
614 - binding: predicate name |
614 - binding: predicate name |