replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;
--- a/src/Pure/Isar/isar_output.ML Thu Jul 27 23:28:26 2006 +0200
+++ b/src/Pure/Isar/isar_output.ML Thu Jul 27 23:28:27 2006 +0200
@@ -436,7 +436,7 @@
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
-fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
+fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
fun pretty_term_typ ctxt t =
ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));