# HG changeset patch
# User wenzelm
# Date 1164310413 -3600
# Node ID 145beb88536a8476d4b46571201d45198cafbb3f
# Parent  a29412af6aa3cf5ae6a6cfedcd42241e0294860e
removed obsolete alphanum;

diff -r a29412af6aa3 -r 145beb88536a src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Nov 23 20:33:32 2006 +0100
+++ b/src/Pure/General/symbol.ML	Thu Nov 23 20:33:33 2006 +0100
@@ -64,7 +64,6 @@
   val default_raw: string -> string
   val xsymbolsN: string
   val symbol_output: string -> string * real
-  val alphanum: string -> string
 end;
 
 structure Symbol: SYMBOL =
@@ -493,26 +492,6 @@
   in implode (rev ss' @ qs) end;
 
 
-(*turning arbitrary names into alphanumerics*)
-
-fun alphanum s =
-  let
-    fun replace_invalid c (last_inv, cs) =
-      if (is_ascii_letter c orelse is_ascii_digit c orelse c = "'")
-        andalso not ("." = c)   (* FIXME !? *)
-      then (false, if last_inv then c :: "_" :: cs else c :: cs)
-      else (true, cs);
-    fun prefix_num_empty [] = ["x"]
-      | prefix_num_empty (cs as c::_) =
-          if is_ascii_digit c
-          then "x" :: cs
-          else cs;
-    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
-    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
-    val cs3 = prefix_num_empty cs2;
-  in implode (prefix :: cs3) end;
-
-
 
 (** print modes **)