# HG changeset patch
# User wenzelm
# Date 961970072 -7200
# Node ID bc3742f62b8004270001e633823be6d8e97f33da
# Parent  52286129faa5fda05c6fee1f96cf4ddc21c635b3
added extern_skolem;

diff -r 52286129faa5 -r bc3742f62b80 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jun 25 23:54:13 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 25 23:54:32 2000 +0200
@@ -28,6 +28,7 @@
   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
@@ -382,7 +383,8 @@
 
 (* 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
@@ -406,6 +408,21 @@
   | 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 **)