Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
print raw (internal) result names;
authorwenzelm
Fri, 12 Sep 2008 12:04:19 +0200
changeset 28211 07cfaa1a9e12
parent 28210 c164d1892553
child 28212 44831b583999
print raw (internal) result names;
src/Pure/Isar/find_theorems.ML file | annotate | diff | comparison | revisions 
--- 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"]
isabelle