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 *)