# HG changeset patch
# User Achim D. Brucker <adbrucker@0x5f.org>
# Date 1658733861 -3600
# Node ID 91cdf474b64d4f4be36f6d2af3182bd367140d31
# Parent  048bbe0bf807a07159714e59feab94283aa305b5
Support 'late use' of Code_Real_Approx_By_Float.

diff -r 048bbe0bf807 -r 91cdf474b64d src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sat Jul 23 12:19:45 2022 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Jul 25 08:24:21 2022 +0100
@@ -20,6 +20,8 @@
   purposes.
 \<close>
 
+code_reserved SML Real
+
 code_printing
   type_constructor real \<rightharpoonup>
     (SML) "real"
@@ -183,16 +185,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"