# HG changeset patch
# User wenzelm
# Date 1656168684 -7200
# Node ID aeb4120657429330d13ef8024f56b808ada20a53
# Parent  44815dc2b8f9fc9e3fca9bc0818c50c49889dab2
prefer antiquotations;

diff -r 44815dc2b8f9 -r aeb412065742 src/Pure/General/base64.ML
--- 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;
diff -r 44815dc2b8f9 -r aeb412065742 src/Pure/General/xz.ML
--- 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;
diff -r 44815dc2b8f9 -r aeb412065742 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jun 25 13:19:15 2022 +0200
+++ b/src/Pure/ROOT.ML	Sat Jun 25 16:51:24 2022 +0200
@@ -300,8 +300,6 @@
 ML_file "System/scala.ML";
 ML_file "System/process_result.ML";
 ML_file "System/isabelle_system.ML";
-ML_file "General/base64.ML";
-ML_file "General/xz.ML";
 
 
 (*theory documents*)
@@ -347,6 +345,8 @@
 
 subsection "Miscellaneous tools and packages for Pure Isabelle";
 
+ML_file "General/base64.ML";
+ML_file "General/xz.ML";
 ML_file "Tools/build.ML";
 ML_file "Tools/named_thms.ML";
 ML_file "Tools/print_operation.ML";