changeset 71379 | 942cc80ba18a |
parent 69458 | 5655af3ea5bd |
child 73136 | ca17e9ebfdf1 |
--- a/src/Pure/ROOT.scala Wed Jan 15 15:05:33 2020 +0100 +++ b/src/Pure/ROOT.scala Wed Jan 15 16:18:24 2020 +0100 @@ -18,7 +18,6 @@ val quote = Library.quote _ val commas = Library.commas _ val commas_quote = Library.commas_quote _ - def proper[A](x: A): Option[A] = Library.proper(x) val proper_string = Library.proper_string _ def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list) }