author | wenzelm |
Sat, 02 Jan 2021 16:09:45 +0100 | |
changeset 73026 | 237bd6318cc1 |
parent 73025 | 3e5a61d9f46a |
child 73027 | 000bcf2524fd |
--- 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)