# HG changeset patch
# User wenzelm
# Date 1208463750 -7200
# Node ID 2e1c3a0e730841309e3fabc3c4090324f9ef6792
# Parent  8690e75e1395bdcc2a8c8eb11359d5dc00343a68
revert_skolem: do not change non-reversible names;
default token translations: revert_skolem;
removed obsolete revert_skolems;

diff -r 8690e75e1395 -r 2e1c3a0e7308 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Apr 17 22:22:28 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 17 22:22:30 2008 +0200
@@ -49,7 +49,6 @@
   val cert_typ_abbrev: Proof.context -> typ -> typ
   val get_skolem: Proof.context -> string -> string
   val revert_skolem: Proof.context -> string -> string
-  val revert_skolems: Proof.context -> term -> term
   val infer_type: Proof.context -> string -> typ
   val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
@@ -347,37 +346,21 @@
   else x;
 
 
-(* revert Skolem constants -- approximation only! *)
+(* revert Skolem constants -- if possible *)
 
-fun revert_skolem ctxt =
-  let
-    val rev_fixes = map Library.swap (Variable.fixes_of ctxt);
-    val revert = AList.lookup (op =) rev_fixes;
-  in
-    fn x =>
-      (case revert x of
-        SOME x' => x'
-      | NONE => perhaps (try Name.dest_skolem) x)
-   end;
-
-fun revert_skolems ctxt =
-  let
-    val revert = revert_skolem ctxt;
-    fun reverts (Free (x, T)) = Free (revert x, T)
-      | reverts (t $ u) = reverts t $ reverts u
-      | reverts (Abs (x, T, t)) = Abs (x, T, reverts t)
-      | reverts a = a;
-  in reverts end;
+fun revert_skolem ctxt x =
+  (case find_first (fn (_, y) => y = x) (Variable.fixes_of ctxt) of
+    SOME (x', _) => if lookup_skolem ctxt x' = SOME x then x' else x
+  | NONE => x);
 
 
 (* default token translations *)
 
 local
 
-fun free_or_skolem ctxt x =   (* FIXME revert skolem *)
-  (case try Name.dest_skolem x of
-    NONE => Pretty.mark Markup.free (Pretty.str x)
-  | SOME x' => Pretty.mark Markup.skolem (Pretty.str x'))
+fun free_or_skolem ctxt x =
+  (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
+   else Pretty.mark Markup.free (Pretty.str x))
   |> Pretty.mark (if Variable.is_fixed ctxt x then Markup.fixed x else Markup.hilite);
 
 fun var_or_skolem _ s =