added internal, dest_internal;

--- a/src/Pure/Syntax/lexicon.ML	Wed Jul 12 16:44:34 2000 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Jul 13 11:36:29 2000 +0200
@@ -24,6 +24,8 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
+  val internal: string -> string
+  val dest_internal: string -> string
   val skolem: string -> string
   val dest_skolem: string -> string
   val read_nat: string -> int option
@@ -327,6 +329,9 @@
 
 (* variable kinds *)
 
+val internal = suffix "_";
+val dest_internal = unsuffix "_";
+
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";