# HG changeset patch
# User wenzelm
# Date 1657105713 -7200
# Node ID ea4f5b0ef497365b6c0b0012f006a3237ab6f1f6
# Parent  c4a1088d008180bfd82ff93a32e709778518f25b
minor performance tuning: avoid redundant BigInt construction;

diff -r c4a1088d0081 -r ea4f5b0ef497 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 05 17:54:52 2022 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 06 13:08:33 2022 +0200
@@ -605,14 +605,13 @@
     def toList: List[A] = array.toList.asInstanceOf[List[A]]
     override def toString: String = array.mkString("Array.T(", ",", ")")
   }
-  def make[A](n: BigInt)(f: BigInt => A): T[A] =
-  {
-    val m = n.toInt
-    val a = new T[A](m)
-    for (i <- 0 until m) a(i) = f(i)
+  def init[A](n: Int)(f: Int => A): T[A] = {
+    val a = new T[A](n)
+    for (i <- 0 until n) a(i) = f(i)
     a
   }
-  def alloc[A](n: BigInt)(x: A): T[A] = make(n)(_ => x)
+  def make[A](n: BigInt)(f: BigInt => A): T[A] = init(n.toInt)((i: Int) => f(BigInt(i)))
+  def alloc[A](n: BigInt)(x: A): T[A] = init(n.toInt)(_ => x)
   def len[A](a: T[A]): BigInt = BigInt(a.length)
   def nth[A](a: T[A], n: BigInt): A = a(n.toInt)
   def upd[A](a: T[A], n: BigInt, x: A): Unit = a.update(n.toInt, x)