ProofContext.legacy_pretty_thm;

--- a/src/Pure/Isar/proof_display.ML	Thu Jul 27 13:43:12 2006 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Jul 27 13:43:13 2006 +0200
@@ -32,7 +32,7 @@
 structure ProofDisplay: PROOF_DISPLAY =
 struct
 
-(* ML toplevel pretty printing *)
+(* toplevel pretty printing *)
 
 val debug = ref false;
 
@@ -47,7 +47,7 @@
 val pprint_term = pprint ProofContext.pretty_term;
 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-fun pprint_thm th = pprint ProofContext.pretty_thm (Thm.theory_of_thm th) th;
+val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true;
 
 
 (* theorems and theory *)

--- a/src/Pure/Thy/html.ML	Thu Jul 27 13:43:12 2006 +0200
+++ b/src/Pure/Thy/html.ML	Thu Jul 27 13:43:13 2006 +0200
@@ -411,15 +411,9 @@
 
 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 smart_pretty_thm;
+    setmp show_question_marks false (ProofContext.legacy_pretty_thm false);
 
 fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));