# HG changeset patch
# User wenzelm
# Date 1150565880 -7200
# Node ID 5be127990076ec82813e07c2c469ccbcb9f34c2e
# Parent  8b4869928f72222b087a3371759cfcb9ede30385
moved internal/skolem to term.ML;

diff -r 8b4869928f72 -r 5be127990076 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Jun 17 19:37:59 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Jun 17 19:38:00 2006 +0200
@@ -26,10 +26,6 @@
   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
   val read_xnum: string -> IntInf.int
   val read_idents: string -> string list
@@ -352,12 +348,6 @@
 
 (* specific identifiers *)
 
-val internal = suffix "_";
-val dest_internal = unsuffix "_";
-
-val skolem = suffix "__";
-val dest_skolem = unsuffix "__";
-
 val constN = "\\<^const>";
 val fixedN = "\\<^fixed>";