# HG changeset patch
# User wenzelm
# Date 1221213859 -7200
# Node ID 07cfaa1a9e120cbabf94a4c2d2c114d236941d8c
# Parent  c164d1892553937e407961dc8c93d3763a32110c
print raw (internal) result names;

diff -r c164d1892553 -r 07cfaa1a9e12 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Fri Sep 12 12:04:16 2008 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Fri Sep 12 12:04:19 2008 +0200
@@ -297,8 +297,9 @@
     val lim = the_default (! limit) opt_limit;
     val thms = Library.drop (len - lim, matches);
 
-    fun prt_fact (thmref, thm) =
-      ProofContext.pretty_fact ctxt (Facts.string_of_ref thmref, [thm]);
+    fun prt_fact (thmref, thm) = Pretty.block
+      [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
+        ProofContext.pretty_thm ctxt thm];
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::
      (if null thms then [Pretty.str "nothing found"]