src/Pure/display.ML
changeset 29858 c8cee17d7e50
parent 29606 fedb8be05f24
child 30186 1f836e949ac2
     1.1 --- a/src/Pure/display.ML	Wed Feb 11 14:48:14 2009 +1100
     1.2 +++ b/src/Pure/display.ML	Wed Feb 11 16:03:10 2009 +1100
     1.3 @@ -20,6 +20,7 @@
     1.4    val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
     1.5    val pretty_thm: thm -> Pretty.T
     1.6    val string_of_thm: thm -> string
     1.7 +  val pretty_fact: Facts.ref * thm -> Pretty.T
     1.8    val pretty_thms: thm list -> Pretty.T
     1.9    val pretty_thm_sg: theory -> thm -> Pretty.T
    1.10    val pretty_thms_sg: theory -> thm list -> Pretty.T
    1.11 @@ -92,6 +93,10 @@
    1.12  
    1.13  val string_of_thm = Pretty.string_of o pretty_thm;
    1.14  
    1.15 +fun pretty_fact (thmref, thm) = Pretty.block
    1.16 +  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.17 +   pretty_thm thm];
    1.18 +
    1.19  fun pretty_thms [th] = pretty_thm th
    1.20    | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    1.21