author | paulson |
Fri, 08 Nov 1996 14:07:56 +0100 | |
changeset 2169 | 31ba286f2307 |
parent 2168 | fcf18ada8904 |
child 2170 | c5e460f1ebb4 |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/goals.ML Fri Nov 08 14:04:38 1996 +0100 +++ b/src/Pure/goals.ML Fri Nov 08 14:07:56 1996 +0100 @@ -142,7 +142,7 @@ val th = strip_shyps (implies_intr_list cAs state) val {hyps,prop,sign=sign',...} = rep_thm th val xshyps = extra_shyps th; - in if not check then standard th + in if not check then th else if not (Sign.eq_sg(sign,sign')) then !result_error_ref state ("Signature of proof state has changed!" ^ sign_error (sign,sign'))