prefer antiquotations;
authorwenzelm
Sat, 25 Jun 2022 16:51:24 +0200
changeset 75621 aeb412065742
parent 75620 44815dc2b8f9
child 75622 53b61706749b
prefer antiquotations;
src/Pure/General/base64.ML
src/Pure/General/xz.ML
src/Pure/ROOT.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;
--- 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;
--- 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";