--- a/src/Pure/Isar/proof_display.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue Jul 21 01:03:18 2009 +0200
@@ -35,7 +35,7 @@
let
val thy = Thm.theory_of_thm th;
val flags = {quote = true, show_hyps = false, show_status = true};
- in Display.pretty_thm_aux (Syntax.pp_global thy) flags [] th end;
+ in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
val pp_term = Pretty.quote oo Syntax.pretty_term_global;
@@ -68,7 +68,7 @@
fun pretty_rule ctxt s thm =
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
- Pretty.fbrk, ProofContext.pretty_thm_aux ctxt false thm];
+ Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
val string_of_rule = Pretty.string_of ooo pretty_rule;