488 else (err (Pretty.string_of (Pretty.chunks |
488 else (err (Pretty.string_of (Pretty.chunks |
489 (pretty_goals_local ctxt "" (true, !show_main_goal) (! Display.goals_limit) raw_th @ |
489 (pretty_goals_local ctxt "" (true, !show_main_goal) (! Display.goals_limit) raw_th @ |
490 [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])))); |
490 [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])))); |
491 |
491 |
492 val {hyps, thy, ...} = Thm.rep_thm raw_th; |
492 val {hyps, thy, ...} = Thm.rep_thm raw_th; |
493 val tsig = Sign.tsig_of thy; |
|
494 val casms = List.concat (map #1 (ProofContext.assumptions_of (context_of state))); |
493 val casms = List.concat (map #1 (ProofContext.assumptions_of (context_of state))); |
495 val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms); |
494 val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms); |
496 |
495 |
497 val th = raw_th RS Drule.rev_triv_goal; |
496 val th = raw_th RS Drule.rev_triv_goal; |
498 val ths = Drule.conj_elim_precise (length ts) th |
497 val ths = Drule.conj_elim_precise (length ts) th |
499 handle THM _ => err "Main goal structure corrupted"; |
498 handle THM _ => err "Main goal structure corrupted"; |
500 in |
499 in |
501 conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^ |
500 conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^ |
502 cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps))); |
501 cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps))); |
503 conditional (exists (not o Pattern.matches tsig) (ts ~~ map Thm.prop_of ths)) (fn () => |
502 conditional (exists (not o Pattern.matches thy) (ts ~~ map Thm.prop_of ths)) (fn () => |
504 err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th))); |
503 err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th))); |
505 ths |
504 ths |
506 end; |
505 end; |
507 |
506 |
508 |
507 |