rename legacy_pretty_thm to pretty_thm_legacy;

--- a/src/Pure/Isar/proof_context.ML	Sat Jul 29 00:51:34 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jul 29 00:51:36 2006 +0200
@@ -25,7 +25,7 @@
   val pretty_classrel: context -> class list -> Pretty.T
   val pretty_arity: context -> arity -> Pretty.T
   val pp: context -> Pretty.pp
-  val legacy_pretty_thm: bool -> thm -> Pretty.T
+  val pretty_thm_legacy: bool -> thm -> Pretty.T
   val pretty_thm: context -> thm -> Pretty.T
   val pretty_thms: context -> thm list -> Pretty.T
   val pretty_fact: context -> string * thm list -> Pretty.T
@@ -281,7 +281,7 @@
 fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt,
   pretty_classrel ctxt, pretty_arity ctxt);
 
-fun legacy_pretty_thm quote th =
+fun pretty_thm_legacy quote th =
   let
     val thy = Thm.theory_of_thm th;
     val pp =

--- a/src/Pure/Isar/proof_display.ML	Sat Jul 29 00:51:34 2006 +0200
+++ b/src/Pure/Isar/proof_display.ML	Sat Jul 29 00:51:36 2006 +0200
@@ -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);
-val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true;
+val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy true;
 
 
 (* theorems and theory *)

--- a/src/Pure/Thy/html.ML	Sat Jul 29 00:51:34 2006 +0200
+++ b/src/Pure/Thy/html.ML	Sat Jul 29 00:51:36 2006 +0200
@@ -413,7 +413,7 @@
 
 val string_of_thm =
   Output.output o Pretty.setmp_margin 80 Pretty.string_of o
-    setmp show_question_marks false (ProofContext.legacy_pretty_thm false);
+    setmp show_question_marks false (ProofContext.pretty_thm_legacy false);
 
 fun thm th = preform (prefix_lines "  " (html_mode string_of_thm th));