# HG changeset patch
# User wenzelm
# Date 1305479966 -7200
# Node ID 7e819eb7dabbed615268d310ec6b1851ab0d50b8
# Parent  ba14eafef0775221fdcea5ce8cce99564a79297c
tuned;

diff -r ba14eafef077 -r 7e819eb7dabb src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun May 15 18:59:27 2011 +0200
+++ b/src/Provers/classical.ML	Sun May 15 19:19:26 2011 +0200
@@ -294,8 +294,7 @@
 fun delete' x = delete_tagged_list (joinrules' x);
 
 fun string_of_thm NONE = Display.string_of_thm_without_context
-  | string_of_thm (SOME context) =
-      Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
+  | string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context);
 
 fun make_elim context th =
   if has_fewer_prems 1 th then