# HG changeset patch
# User wenzelm
# Date 756481649 -3600
# Node ID ac55692ab41f5f4aefd0f8ba2bbd75dc1cf7c4e5
# Parent  0f0ff91b07f627df8ca9913de425b90affb60c4c
pretty_thm is now exported;

diff -r 0f0ff91b07f6 -r ac55692ab41f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Dec 21 13:58:12 1993 +0100
+++ b/src/Pure/drule.ML	Tue Dec 21 14:47:29 1993 +0100
@@ -1,4 +1,4 @@
-(*  Title: 	drule
+(*  Title: 	Pure/drule.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -41,6 +41,7 @@
   val print_theory: theory -> unit
   val pprint_sg: Sign.sg -> pprint_args -> unit
   val pprint_theory: theory -> pprint_args -> unit
+  val pretty_thm: thm -> Sign.Syntax.Pretty.T
   val print_thm: thm -> unit
   val prth: thm -> thm
   val prthq: thm Sequence.seq -> thm Sequence.seq