equal
deleted
inserted
replaced
463 |
463 |
464 fun conclude_goal state goal propss = |
464 fun conclude_goal state goal propss = |
465 let |
465 let |
466 val thy = theory_of state; |
466 val thy = theory_of state; |
467 val ctxt = context_of state; |
467 val ctxt = context_of state; |
468 val string_of_term = ProofContext.string_of_term ctxt; |
468 val string_of_term = Syntax.string_of_term ctxt; |
469 val string_of_thm = ProofContext.string_of_thm ctxt; |
469 val string_of_thm = ProofContext.string_of_thm ctxt; |
470 |
470 |
471 val ngoals = Thm.nprems_of goal; |
471 val ngoals = Thm.nprems_of goal; |
472 val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks |
472 val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks |
473 (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @ |
473 (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @ |