diff -r 6889bfc03804 -r 1f836e949ac2 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Mar 01 14:36:27 2009 +0100
+++ b/src/Pure/display.ML	Sun Mar 01 14:45:23 2009 +0100
@@ -20,7 +20,6 @@
   val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
   val pretty_thm: thm -> Pretty.T
   val string_of_thm: thm -> string
-  val pretty_fact: Facts.ref * thm -> Pretty.T
   val pretty_thms: thm list -> Pretty.T
   val pretty_thm_sg: theory -> thm -> Pretty.T
   val pretty_thms_sg: theory -> thm list -> Pretty.T
@@ -93,10 +92,6 @@
 
 val string_of_thm = Pretty.string_of o pretty_thm;
 
-fun pretty_fact (thmref, thm) = Pretty.block
-  [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
-   pretty_thm thm];
-
 fun pretty_thms [th] = pretty_thm th
   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));