moved internal/skolem to term.ML;
authorwenzelm
Sat, 17 Jun 2006 19:38:00 +0200
changeset 19918 5be127990076
parent 19917 8b4869928f72
child 19919 138e0684cda2
moved internal/skolem to term.ML;
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>";