changeset 73026 | 237bd6318cc1 |
parent 73024 | 337e1b135d2f |
child 73031 | f93f0597f4fb |
--- 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)