src/Pure/Tools/find_theorems.ML
changeset 49888 ff2063be8227
parent 48646 91281e9472d8
child 50214 67fb9a168d10
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Oct 17 10:45:43 2012 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 17 10:46:14 2012 +0200
     1.3 @@ -554,12 +554,21 @@
     1.4  val find_theorems = gen_find_theorems filter_theorems;
     1.5  val find_theorems_cmd = gen_find_theorems filter_theorems_cmd;
     1.6  
     1.7 -fun pretty_theorem ctxt (Internal (thmref, thm)) = Pretty.block
     1.8 -      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
     1.9 -        Display.pretty_thm ctxt thm]
    1.10 -  | pretty_theorem ctxt (External (thmref, prop)) = Pretty.block
    1.11 -      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.12 -        Syntax.unparse_term ctxt prop];
    1.13 +fun pretty_ref ctxt thmref =
    1.14 +  let
    1.15 +    val (name, sel) =
    1.16 +      (case thmref of
    1.17 +        Facts.Named ((name, _), sel) => (name, sel)
    1.18 +      | Facts.Fact _ => raise Fail "Illegal literal fact");
    1.19 +  in
    1.20 +    [Pretty.mark (Proof_Context.markup_fact ctxt name) (Pretty.str name),
    1.21 +      Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1]
    1.22 +  end;
    1.23 +
    1.24 +fun pretty_theorem ctxt (Internal (thmref, thm)) =
    1.25 +      Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm])
    1.26 +  | pretty_theorem ctxt (External (thmref, prop)) =
    1.27 +      Pretty.block (pretty_ref ctxt thmref @ [Syntax.unparse_term ctxt prop]);
    1.28  
    1.29  fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
    1.30