src/Pure/Tools/find_theorems.ML
changeset 32091 30e2ffbba718
parent 31687 0d2f700fe5e7
child 32149 ef59550a55d3
--- a/src/Pure/Tools/find_theorems.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -408,7 +408,7 @@
 
 fun pretty_thm ctxt (thmref, thm) = Pretty.block
   [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
-    ProofContext.pretty_thm ctxt thm];
+    Display.pretty_thm ctxt thm];
 
 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let