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