results: smart_pretty_thm uses adhoc proof context if possible;

--- a/src/Pure/Thy/html.ML	Sun Apr 09 18:51:22 2006 +0200
+++ b/src/Pure/Thy/html.ML	Sun Apr 09 18:51:23 2006 +0200
@@ -411,9 +411,15 @@
 
 local
 
+fun smart_pretty_thm th =
+  let val thy = Thm.theory_of_thm th in
+    if eq_thy (thy, ProtoPure.thy) then Display.pretty_thm_no_quote th
+    else ProofContext.pretty_thm (ProofContext.init thy) th
+  end;
+
 val string_of_thm =
   Output.output o Pretty.setmp_margin 80 Pretty.string_of o
-    setmp show_question_marks false Display.pretty_thm_no_quote;
+    setmp show_question_marks false smart_pretty_thm;
 
 fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));