# HG changeset patch
# User wenzelm
# Date 1085167330 -7200
# Node ID e7f7ed4c06f285caa56245a71e37689ab718b2b5
# Parent  d6ce35a1c3866c2acfb537860fcc8ac416d7c9ad
string_of_vname moved to term.ML;

diff -r d6ce35a1c386 -r e7f7ed4c06f2 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri May 21 21:21:51 2004 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Fri May 21 21:22:10 2004 +0200
@@ -114,18 +114,8 @@
 
 (** string_of_vname **)
 
-fun string_of_vname (x, i) =
-  let
-    val si = string_of_int i;
-    val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true;
-  in
-    if dot then "?" ^ x ^ "." ^ si
-    else if i = 0 then "?" ^ x
-    else "?" ^ x ^ si
-  end;
-
-fun string_of_vname' (x, ~1) = x
-  | string_of_vname' xi = string_of_vname xi;
+val string_of_vname = Term.string_of_vname;
+val string_of_vname' = Term.string_of_vname';
 
 
 
@@ -270,10 +260,10 @@
   Scan.lift ($$ "*" --| Scan.ahead (Scan.one (not_equal ")"))) ||
   Scan.lift (Scan.one (not_equal "*" andf Symbol.not_eof));
 
-fun scan_comment xs =
-  ($$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
+val scan_comment =
+  $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
     (Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")")
-   >> K None) xs;
+  >> K ();
 
 
 
@@ -297,7 +287,7 @@
     val scan_lit = Scan.literal lex >> (pair Token o implode);
 
     val scan_token =
-      scan_comment ||
+      scan_comment >> K None ||
       Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => Some (tk s)) ||
       scan_str >> (Some o StrSy o implode_xstr) ||
       Scan.one Symbol.is_blank >> K None;
diff -r d6ce35a1c386 -r e7f7ed4c06f2 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri May 21 21:21:51 2004 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri May 21 21:22:10 2004 +0200
@@ -65,7 +65,7 @@
 
 fun simple_ast_of (Const (c, _)) = Ast.Constant c
   | simple_ast_of (Free (x, _)) = Ast.Variable x
-  | simple_ast_of (Var (xi, _)) = Ast.Variable (Lexicon.string_of_vname xi)
+  | simple_ast_of (Var (xi, _)) = Ast.Variable (Term.string_of_vname xi)
   | simple_ast_of (t as _ $ _) =
       let val (f, args) = strip_comb t in
         Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)