1.1 --- a/src/Pure/Thy/html.ML	Sun Apr 09 18:51:22 2006 +0200
     1.2 +++ b/src/Pure/Thy/html.ML	Sun Apr 09 18:51:23 2006 +0200
     1.3 @@ -411,9 +411,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun smart_pretty_thm th =
     1.8 +  let val thy = Thm.theory_of_thm th in
     1.9 +    if eq_thy (thy, ProtoPure.thy) then Display.pretty_thm_no_quote th
    1.10 +    else ProofContext.pretty_thm (ProofContext.init thy) th
    1.11 +  end;
    1.12 +
    1.13  val string_of_thm =
    1.14    Output.output o Pretty.setmp_margin 80 Pretty.string_of o
    1.15 -    setmp show_question_marks false Display.pretty_thm_no_quote;
    1.16 +    setmp show_question_marks false smart_pretty_thm;
    1.17  
    1.18  fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));
    1.19