From e38b007a620dca66fe651b6f48586caf70f68863 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Fri, 25 Oct 2024 11:33:06 +1100
Subject: [PATCH] Make it apparent (with Poly/ML for now) that Arbint.int =
 IntInf.int

---
 src/portableML/Arbint.sig          | 2 +-
 src/portableML/poly/Arbintcore.sig | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/portableML/Arbint.sig b/src/portableML/Arbint.sig
index 3787ff6b5c..adf03ed733 100644
--- a/src/portableML/Arbint.sig
+++ b/src/portableML/Arbint.sig
@@ -1,7 +1,7 @@
 signature Arbint =
 sig
 
-  include Arbintcore where type int = Arbintcore.int
+  include Arbintcore
   val pp_int     : int -> HOLPP.pretty
 
 end
diff --git a/src/portableML/poly/Arbintcore.sig b/src/portableML/poly/Arbintcore.sig
index 09babadc5b..6f8dd2fd2f 100644
--- a/src/portableML/poly/Arbintcore.sig
+++ b/src/portableML/poly/Arbintcore.sig
@@ -1,7 +1,7 @@
 signature Arbintcore =
 sig
 
-  eqtype int
+  type int = IntInf.int
 
   type num = Arbnumcore.num