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