src/Pure/Syntax/lexicon.ML
changeset 22686 68496cc300a4
parent 22574 e6c25fd3de2a
child 23784 75e6b9dd5336
--- a/src/Pure/Syntax/lexicon.ML	Sat Apr 14 17:36:17 2007 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Apr 14 17:36:18 2007 +0200
@@ -21,8 +21,6 @@
   val scan_int: string list -> string * string list
   val scan_hex: string list -> string * string list
   val scan_bin: string list -> string * string list
-  val string_of_vname: indexname -> string
-  val string_of_vname': indexname -> string
   val read_indexname: string -> indexname
   val read_var: string -> term
   val read_variable: string -> indexname option
@@ -114,13 +112,6 @@
 
 
 
-(** string_of_vname **)
-
-val string_of_vname = Term.string_of_vname;
-val string_of_vname' = Term.string_of_vname';
-
-
-
 (** datatype token **)
 
 datatype token =