X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautLexer.mll;h=58324a0216c71e2c693a3d0ca5169a2a7a193e93;hb=c450fdfb1b02eb69e5e7ef25f0acdf80157710df;hp=5a7155e4a56db66a0aa153c02b9b8cd121180856;hpb=586c361209ac14e8c2b1da3509041c0c82a86c92;p=helm.git

diff --git a/helm/software/helena/src/automath/autLexer.mll b/helm/software/helena/src/automath/autLexer.mll
index 5a7155e4a..58324a021 100644
--- a/helm/software/helena/src/automath/autLexer.mll
+++ b/helm/software/helena/src/automath/autLexer.mll
@@ -10,6 +10,8 @@
       V_______________________________________________________________ *)
 
 { 
+   module KT = String
+
    module L  = Log
    module G  = Options
    module AP = AutParser
@@ -23,15 +25,12 @@ END
 IFDEF QUOTE THEN
 (* This turns an Automath identifier into an XML nmtoken *)
    let quote id =
-      let l = String.length id in
-      let rec aux i =
-         if i < l then begin
-            if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
-	    aux (succ i)
-         end else
-	    id
+      let map = function
+         | '\''
+         | '`' -> '_';
+         | c   -> c
       in
-      aux 0
+      KT.map map id
 
 END
 }