Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/auto_solve.ML
changeset 30186 1f836e949ac2
parent 30147 c1e1d96903ea
child 30242 aea5d7fa7ef5 
--- a/src/Tools/auto_solve.ML	Sun Mar 01 14:36:27 2009 +0100
+++ b/src/Tools/auto_solve.ML	Sun Mar 01 14:45:23 2009 +0100
@@ -45,7 +45,7 @@
                   | SOME g => Syntax.string_of_term ctxt (term_of g);
       in
         Pretty.big_list (msg ^ " could be solved directly with:")
-                        (map Display.pretty_fact results)
+                        (map (FindTheorems.pretty_thm ctxt) results)
       end;
 
     fun seek_against_goal () =
isabelle