equal
deleted
inserted
replaced
119 |
119 |
120 fun prep_thm_axm thy thm = |
120 fun prep_thm_axm thy thm = |
121 let |
121 let |
122 fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]); |
122 fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]); |
123 |
123 |
124 val {sign, shyps, hyps, prop, ...} = rep_thm thm; |
124 val {sign, hyps, prop, ...} = rep_thm thm; |
125 in |
125 in |
126 if not (Sign.subsig (sign, sign_of thy)) then |
126 if not (Sign.subsig (sign, sign_of thy)) then |
127 err "theorem not of same theory" |
127 err "theorem not of same theory" |
128 else if not (null shyps) orelse not (null hyps) then |
128 else if not (null (extra_shyps thm)) orelse not (null hyps) then |
129 err "theorem may not contain hypotheses" |
129 err "theorem may not contain hypotheses" |
130 else prop |
130 else prop |
131 end; |
131 end; |
132 |
132 |
133 (*general theorems*) |
133 (*general theorems*) |