src/Pure/General/scan.scala
changeset 46712 8650d9a95736
parent 46627 fbe2cb05bdb3
child 48342 4a8f06cbf8bb
--- a/src/Pure/General/scan.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/General/scan.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -40,7 +40,7 @@
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
-  class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
+  final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
   {
     import Lexicon.Tree