# HG changeset patch
# User wenzelm
# Date 1350463574 -7200
# Node ID ff2063be8227a50676d5b6f2d6bde56cfdce7a3b
# Parent  1a173b2503c0a4d403eb705b8da2a92d9628194b
more formal markup;

diff -r 1a173b2503c0 -r ff2063be8227 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Oct 17 10:45:43 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Oct 17 10:46:14 2012 +0200
@@ -51,6 +51,7 @@
   val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val extern_fact: Proof.context -> string -> xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
+  val markup_fact: Proof.context -> string -> Markup.T
   val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val read_class: Proof.context -> xstring -> class
diff -r 1a173b2503c0 -r ff2063be8227 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Oct 17 10:45:43 2012 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 17 10:46:14 2012 +0200
@@ -554,12 +554,21 @@
 val find_theorems = gen_find_theorems filter_theorems;
 val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
 
-fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
-      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
-        Display.pretty_thm ctxt thm]
-  | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
-      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
-        Syntax.unparse_term ctxt prop];
+fun pretty_ref ctxt thmref =
+  let
+    val (name, sel) =
+      (case thmref of
+        Facts.Named ((name, _), sel) => (name, sel)
+      | Facts.Fact _ => raise Fail "Illegal literal fact");
+  in
+    [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
+      Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
+  end;
+
+fun pretty_theorem ctxt (Internal (thmref, thm)) =
+      Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
+  | pretty_theorem ctxt (External (thmref, prop)) =
+      Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
 
 fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));