equal
deleted
inserted
replaced
1690 val t = Logic.mk_conjunction_balanced ts; |
1690 val t = Logic.mk_conjunction_balanced ts; |
1691 val body = ObjectLogic.atomize_term thy t; |
1691 val body = ObjectLogic.atomize_term thy t; |
1692 val bodyT = Term.fastype_of body; |
1692 val bodyT = Term.fastype_of body; |
1693 in |
1693 in |
1694 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) |
1694 if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) |
1695 else (body, bodyT, ObjectLogic.atomize_cterm (Thm.cterm_of thy t)) |
1695 else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t)) |
1696 end; |
1696 end; |
1697 |
1697 |
1698 fun aprop_tr' n c = (c, fn args => |
1698 fun aprop_tr' n c = (c, fn args => |
1699 if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args) |
1699 if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args) |
1700 else raise Match); |
1700 else raise Match); |