src/Pure/General/word.scala
changeset 82120 a4aa45999dd7
parent 81647 ae670d860912
child 82124 1eda03781f76
--- a/src/Pure/General/word.scala	Sun Feb 09 12:14:09 2025 +0100
+++ b/src/Pure/General/word.scala	Sun Feb 09 12:35:29 2025 +0100
@@ -77,10 +77,4 @@
     explode(Character.isWhitespace _, text)
 
   def informal(text: String): String = implode(explode('_', text))
-
-
-  /* brackets */
-
-  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"
-  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"
 }