137 !print_goals_ref (!goals_limit) state; |
137 !print_goals_ref (!goals_limit) state; |
138 error msg) |
138 error msg) |
139 (*discharges assumptions from state in the order they appear in goal; |
139 (*discharges assumptions from state in the order they appear in goal; |
140 checks (if requested) that resulting theorem is equivalent to goal. *) |
140 checks (if requested) that resulting theorem is equivalent to goal. *) |
141 fun mkresult (check,state) = |
141 fun mkresult (check,state) = |
142 let val ngoals = nprems_of state |
142 let val state = Sequence.hd (flexflex_rule state) |
|
143 handle _ => state (*smash flexflex pairs*) |
|
144 val ngoals = nprems_of state |
143 val th = implies_intr_list cAs state |
145 val th = implies_intr_list cAs state |
144 val {hyps,prop,sign=sign',...} = rep_thm th |
146 val {hyps,prop,sign=sign',...} = rep_thm th |
145 in if not check then standard th |
147 in if not check then standard th |
146 else if not (Sign.eq_sg(sign,sign')) then result_error state |
148 else if not (Sign.eq_sg(sign,sign')) then result_error state |
147 ("Signature of proof state has changed!" ^ |
149 ("Signature of proof state has changed!" ^ |