# HG changeset patch
# User wenzelm
# Date 963480989 -7200
# Node ID be6e79d1aae0e8e8f59e74a3bb3c7480f503398e
# Parent  06a55195741bd546c04c7be9de8fc9c96d6f185d
added internal, dest_internal;

diff -r 06a55195741b -r be6e79d1aae0 src/Pure/Syntax/lexicon.ML
--- 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 "__";