# HG changeset patch
# User wenzelm
# Date 1176564978 -7200
# Node ID 68496cc300a4bd1553e9f083617a898f9fee7f92
# Parent  fc4ef3807fb9e274c7a824605dfd6e8a83183ab8
removed redundant string_of_vname (see term.ML);

diff -r fc4ef3807fb9 -r 68496cc300a4 src/Pure/Syntax/lexicon.ML
--- 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 =