src/Provers/classical.ML
changeset 42817 7e819eb7dabb
parent 42812 dda4aef7cba4
child 45375 7fe19930dfc9
     1.1 --- a/src/Provers/classical.ML	Sun May 15 18:59:27 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Sun May 15 19:19:26 2011 +0200
     1.3 @@ -294,8 +294,7 @@
     1.4  fun delete' x = delete_tagged_list (joinrules' x);
     1.5  
     1.6  fun string_of_thm NONE = Display.string_of_thm_without_context
     1.7 -  | string_of_thm (SOME context) =
     1.8 -      Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
     1.9 +  | string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context);
    1.10  
    1.11  fun make_elim context th =
    1.12    if has_fewer_prems 1 th then