--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Jul 22 18:26:52 2022 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Jul 25 08:29:23 2022 +0100
@@ -20,6 +20,8 @@
   purposes.
 \<close>
 
+code_reserved SML Real
+
 code_printing
   type_constructor real \<rightharpoonup>
     (SML) "real"
@@ -204,16 +206,22 @@
 code_printing
   constant Ratreal \<rightharpoonup> (SML)
 
-definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
-  where "Realfract p q = of_int p / of_int q"
+definition Realfract :: "real \<Rightarrow> real \<Rightarrow> real"
+  where "Realfract p q = p / q"
+
+definition Realfract' :: "int \<Rightarrow> int \<Rightarrow> real"
+  where "Realfract' p q = Realfract (of_int p) (of_int q)"
+
+
 
 code_datatype Realfract
 
 code_printing
-  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
+  constant Realfract \<rightharpoonup> (SML) "_/ '// _"
+
 
-lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
-  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
+lemma [code]: "Ratreal r = case_prod Realfract' (quotient_of r)"
+  by (cases r) (simp add: Realfract_def Realfract'_def quotient_of_Fract of_rat_rat)
 
 declare [[code drop: "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
   "plus :: real \<Rightarrow> real \<Rightarrow> real"

--- a/src/Pure/ROOT.ML	Fri Jul 22 18:26:52 2022 +0100
+++ b/src/Pure/ROOT.ML	Mon Jul 25 08:29:23 2022 +0100
@@ -363,5 +363,4 @@
 ML_file "Tools/doc.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
-ML_file "Tools/scala_build.ML";
 ML_file "Tools/generated_files.ML";

--- a/src/Pure/System/isabelle_system.scala	Fri Jul 22 18:26:52 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Jul 25 08:29:23 2022 +0100
@@ -55,32 +55,37 @@
 
   /* init settings + services */
 
-  def get_services(): List[Class[Service]] = {
-    def make(where: String, names: List[String]): List[Class[Service]] = {
-      for (name <- names) yield {
-        def err(msg: String): Nothing =
-          error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
-        try { Class.forName(name).asInstanceOf[Class[Service]] }
-        catch {
-          case _: ClassNotFoundException => err("Class not found")
-          case exn: Throwable => err(Exn.message(exn))
-        }
+  private def init_services(where: String, names: List[String]): List[Class[Service]] = {
+    for (name <- names) yield {
+      def err(msg: String): Nothing =
+        error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
+      try { Class.forName(name).asInstanceOf[Class[Service]] }
+      catch {
+        case _: ClassNotFoundException => err("Class not found")
+        case exn: Throwable => err(Exn.message(exn))
       }
     }
-
-    def from_env(variable: String): List[Class[Service]] =
-      make(quote(variable), space_explode(':', getenv_strict(variable)))
+  }
 
-    def from_jar(platform_jar: String): List[Class[Service]] =
-      make(quote(platform_jar),
-        isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList)
+  def init_services_env(): List[Class[Service]] =
+  {
+    val variable = "ISABELLE_SCALA_SERVICES"
+    init_services(quote(variable), space_explode(':', getenv_strict(variable)))
+  }
 
-    from_env("ISABELLE_SCALA_SERVICES") ::: Scala.get_classpath().flatMap(from_jar)
-  }
+  def init_services_jar(jar: Path): List[Class[Service]] =
+    init_services(jar.toString, isabelle.setup.Build.get_services(jar.java_path).asScala.toList)
+
+  def init_services_jar(platform_jar: String): List[Class[Service]] =
+    init_services_jar(Path.explode(File.standard_path(platform_jar)))
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = {
     isabelle.setup.Environment.init(isabelle_root, cygwin_root)
-    synchronized { if (_services.isEmpty) { _services = Some(get_services()) } }
+    synchronized {
+      if (_services.isEmpty) {
+        _services = Some(init_services_env() ::: Scala.get_classpath().flatMap(init_services_jar))
+      }
+    }
   }
 
 

--- a/src/Pure/Tools/generated_files.ML	Fri Jul 22 18:26:52 2022 +0100
+++ b/src/Pure/Tools/generated_files.ML	Mon Jul 25 08:29:23 2022 +0100
@@ -304,7 +304,14 @@
       val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
       val _ = List.app (write_file dir o #1) files;
       val _ = List.app (get_external_files dir) external;
-    in Scala_Build.scala_build ctxt dir end);
+      val [jar_name, jar_bytes, output] =
+        \<^scala>\<open>scala_build\<close> [Bytes.string (Isabelle_System.absolute_path dir)];
+      val _ = writeln (Bytes.content output);
+    in
+      Export.export (Proof_Context.theory_of ctxt)
+        (Path.explode_binding0 (Bytes.content jar_name))
+        (Bytes.contents_blob jar_bytes)
+    end);
 
 fun scala_build_generated_files_cmd ctxt args external =
   scala_build_generated_files ctxt

--- a/src/Pure/Tools/scala_build.ML	Fri Jul 22 18:26:52 2022 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(*  Title:      Pure/Tools/scala_build.ML
-    Author:     Makarius
-
-Build and export Isabelle/Scala/Java modules.
-*)
-
-signature SCALA_BUILD =
-sig
-  val scala_build: Proof.context -> Path.T -> unit
-end
-
-structure Scala_Build: SCALA_BUILD =
-struct
-
-fun scala_build ctxt dir =
-  let
-    val [jar_name, jar_bytes, output] =
-      \<^scala>\<open>scala_build\<close> [Bytes.string (Isabelle_System.absolute_path dir)];
-    val _ = writeln (Bytes.content output);
-  in
-    Export.export (Proof_Context.theory_of ctxt)
-      (Path.explode_binding0 (Bytes.content jar_name))
-      (Bytes.contents_blob jar_bytes)
-  end;
-
-end;