| changeset 75621 | aeb412065742 |
| parent 75620 | 44815dc2b8f9 |
| child 76183 | 8089593a364a |
--- a/src/Pure/General/base64.ML Sat Jun 25 13:19:15 2022 +0200 +++ b/src/Pure/General/base64.ML Sat Jun 25 16:51:24 2022 +0200 @@ -13,7 +13,7 @@ structure Base64: BASE64 = struct -val decode = Scala.function1_bytes "Base64.decode"; -val encode = Scala.function1_bytes "Base64.encode"; +val decode = \<^scala>\<open>Base64.decode\<close>; +val encode = \<^scala>\<open>Base64.encode\<close>; end;