# HG changeset patch
# User wenzelm
# Date 1144601483 -7200
# Node ID 5cfa11eeddfed9e6d1bcb87de1511fe4a1d89b9e
# Parent  6af442fa80c30aa0a4ccc837e20e369b9af8089d
results: smart_pretty_thm uses adhoc proof context if possible;

diff -r 6af442fa80c3 -r 5cfa11eeddfe src/Pure/Thy/html.ML
--- 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));