src/Pure/General/symbol.scala
changeset 73606 d8a0e996614b
parent 73602 ec52a1a6ed31
--- a/src/Pure/General/symbol.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/symbol.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -336,14 +336,14 @@
     }
 
     private val symbols: List[(Symbol, Properties.T)] =
-      (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /:
-          split_lines(symbols_spec).reverse)
-        { case (res, No_Decl()) => res
+      split_lines(symbols_spec).reverse.
+        foldLeft((List.empty[(Symbol, Properties.T)], Set.empty[Symbol])) {
+          case (res, No_Decl()) => res
           case ((list, known), decl) =>
             val (sym, props) = read_decl(decl)
             if (known(sym)) (list, known)
             else ((sym, props) :: list, known + sym)
-        })._1
+        }._1
 
 
     /* basic properties */