# HG changeset patch
# User wenzelm
# Date 1609600185 -3600
# Node ID 237bd6318cc1ee5a158b0fe7f35dc1520952518b
# Parent  3e5a61d9f46a6ffaedfa4547c30f858aedaa9a72
more uniform default --- hardly relevant in practice;

diff -r 3e5a61d9f46a -r 237bd6318cc1 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)