Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned append;
authorwenzelm
Tue, 26 Aug 2008 16:36:30 +0200
changeset 28007 2d0c93291293
parent 28006 116b9c1d402f
child 28008 f945f8d9ad4d
tuned append;
src/Pure/General/symbol.scala file | annotate | diff | comparison | revisions
src/Pure/General/xml.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/symbol.scala	Tue Aug 26 16:36:11 2008 +0200
+++ b/src/Pure/General/symbol.scala	Tue Aug 26 16:36:30 2008 +0200
@@ -148,7 +148,7 @@
 
     private def init_recoders() = {
       val list = symbols.elements.toList.map(get_code)
-      decoder = new Recoder(list ::: (for ((x, y) <- list) yield ("\\" + x, y)))
+      decoder = new Recoder(list ++ (for ((x, y) <- list) yield ("\\" + x, y)))
       encoder = new Recoder(for ((x, y) <- list) yield (y, x))
     }
 
--- a/src/Pure/General/xml.scala	Tue Aug 26 16:36:11 2008 +0200
+++ b/src/Pure/General/xml.scala	Tue Aug 26 16:36:30 2008 +0200
@@ -33,7 +33,7 @@
     case Nil => None
     case t :: ts => get_next(t) match {
       case None => get_nexts(ts)
-      case Some((s, r)) => Some((s, r ::: ts))
+      case Some((s, r)) => Some((s, r ++ ts))
     }
   }
isabelle