src/Pure/Isar/proof_context.ML

   val assumptions: context -> (cterm * ((int -> tactic) * (int -> tactic))) list
   val fixed_names: context -> string list
   val read_typ: context -> string -> typ
   val cert_typ: context -> typ -> typ
   val cert_skolem: context -> string -> string
+  val extern_skolem: context -> term -> term
   val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
   val read_term: context -> string -> term
   val read_prop: context -> string -> term
   val read_termT_pats: context -> (string * typ) list -> term list
   val read_term_pats: typ -> context -> string list -> term list

     handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
 
 
 (* internalize Skolem constants *)
 
-fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x);
+fun fixes_of (Context {asms = (_, (fixes, _)), ...}) = fixes;
+fun get_skolem ctxt x = assoc (fixes_of ctxt, x);
 
 fun check_skolem ctxt check x =
   if check andalso can Syntax.dest_skolem x then
     raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
   else x;

 fun cert_skolem ctxt x =
   (case get_skolem ctxt x of
     None => raise CONTEXT ("Undeclared variable: " ^ quote x, ctxt)
   | Some x' => x');
 
+
+(* externalize Skolem constants -- for printing purposes only *)
+
+fun extern_skolem ctxt =
+  let
+    val rev_fixes = map Library.swap (fixes_of ctxt);
+
+    fun extern (t as Free (x, T)) =
+          (case assoc (rev_fixes, x) of
+            Some x' => Free (if get_skolem ctxt x' = Some x then x' else NameSpace.hidden x', T)
+          | None => t)
+      | extern (t $ u) = extern t $ extern u
+      | extern (Abs (x, T, t)) = Abs (x, T, extern t)
+      | extern a = a;
+  in extern end
 
 
 (** prepare terms and propositions **)
 
 (*