# HG changeset patch
# User wenzelm
# Date 1132159535 -3600
# Node ID b44d5308810841203505521b5c18c1a992196901
# Parent  cb53a778455e9402b11a421c87167502341112a3
added deskolem;

diff -r cb53a778455e -r b44d53088108 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Nov 16 17:45:34 2005 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Nov 16 17:45:35 2005 +0100
@@ -30,6 +30,7 @@
   val dest_internal: string -> string
   val skolem: string -> string
   val dest_skolem: string -> string
+  val deskolem: string -> string
   val read_nat: string -> int option
   val read_xnum: string -> IntInf.int
   val read_idents: string -> string list
@@ -355,6 +356,7 @@
 
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
+fun deskolem x = the_default x (try dest_skolem x);
 
 
 (* read_nat *)