# HG changeset patch
# User wenzelm
# Date 1154035707 -7200
# Node ID cfea8e7f9ebdfd7ad260dc50a2c8b17510c75cdc
# Parent  a571d044891e10b9759552b421b2ada85f7966a5
replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;

diff -r a571d044891e -r cfea8e7f9ebd src/Pure/Isar/isar_output.ML
--- 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));