more uniform default --- hardly relevant in practice;
authorwenzelm
Sat, 02 Jan 2021 16:09:45 +0100
changeset 73026 237bd6318cc1
parent 73025 3e5a61d9f46a
child 73027 000bcf2524fd
more uniform default --- hardly relevant in practice;
src/Pure/term.scala
--- a/src/Pure/term.scala	Sat Jan 02 16:07:40 2021 +0100
+++ b/src/Pure/term.scala	Sat Jan 02 16:09:45 2021 +0100
@@ -136,7 +136,7 @@
   object Cache
   {
     def make(
-        max_string: Int = Integer.MAX_VALUE,
+        max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
       new Cache(initial_size, max_string)