removed redundant string_of_vname (see term.ML);
authorwenzelm
Sat, 14 Apr 2007 17:36:18 +0200
changeset 22686 68496cc300a4
parent 22685 fc4ef3807fb9
child 22687 53943f4dab21
removed redundant string_of_vname (see term.ML);
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 =