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/Pure/Isar/proof_context.ML
changeset 14876 477c414000f8
parent 14828 15d12761ba54
child 14901 c7a8a8eb7fc8 
--- a/src/Pure/Isar/proof_context.ML	Sat Jun 05 13:07:49 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jun 05 13:08:53 2004 +0200
@@ -392,7 +392,7 @@
 
 fun pretty_thm ctxt thm =
   if ! Display.show_hyps then
-    Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm
+    Display.pretty_thm_aux (pp ctxt) false thm
   else pretty_term ctxt (Thm.prop_of thm);
 
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
isabelle