--- a/src/Pure/Isar/proof.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/proof.ML Sat Mar 30 13:40:19 2013 +0100
@@ -337,12 +337,7 @@
(** pretty_state **)
fun pretty_facts _ _ NONE = []
- | pretty_facts s ctxt (SOME ths) =
- [(Pretty.block o Pretty.fbreaks)
- ((if s = "" then Pretty.str "this:"
- else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
- map (Display.pretty_thm ctxt) ths),
- Pretty.str ""];
+ | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
fun pretty_state nr state =
let
@@ -351,7 +346,7 @@
fun prt_goal (SOME (_, (_,
{statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
- pretty_facts "using" ctxt
+ pretty_facts ctxt "using"
(if mode <> Backward orelse null using then NONE else SOME using) @
[Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
(map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
@@ -367,8 +362,8 @@
Pretty.str ""] @
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then
- pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
- else if mode = Chain then pretty_facts "picking" ctxt facts
+ pretty_facts ctxt "" facts @ prt_goal (try find_goal state)
+ else if mode = Chain then pretty_facts ctxt "picking" facts
else prt_goal (try find_goal state))
end;