changeset 74265 | 633fe7390c97 |
parent 74249 | 9d9e7ed01dbb |
child 74266 | 612b7e0d6721 |
--- a/src/Pure/more_thm.ML Wed Sep 08 08:41:36 2021 +0200 +++ b/src/Pure/more_thm.ML Thu Sep 09 10:40:57 2021 +0200 @@ -218,7 +218,7 @@ ||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of; -(* tables and caches *) +(* scalable collections *) structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); structure Thmtab = Table(type key = thm val ord = thm_ord);