equal
deleted
inserted
replaced
378 fun simple_prove_goal_cterm G f = |
378 fun simple_prove_goal_cterm G f = |
379 let |
379 let |
380 val _ = warn_obsolete (); |
380 val _ = warn_obsolete (); |
381 val As = Drule.strip_imp_prems G; |
381 val As = Drule.strip_imp_prems G; |
382 val B = Drule.strip_imp_concl G; |
382 val B = Drule.strip_imp_concl G; |
383 val asms = map (Goal.norm_hhf o Thm.assume) As; |
383 val asms = map Assumption.assume As; |
384 fun check NONE = error "prove_goal: tactic failed" |
384 fun check NONE = error "prove_goal: tactic failed" |
385 | check (SOME (thm, _)) = (case nprems_of thm of |
385 | check (SOME (thm, _)) = (case nprems_of thm of |
386 0 => thm |
386 0 => thm |
387 | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!")) |
387 | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!")) |
388 in |
388 in |