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