| changeset 74270 | ad2899cdd528 |
| parent 67721 | 5348bea4accd |
| child 74518 | de4f151c2a34 |
--- a/src/Pure/conv.ML Thu Sep 09 14:50:26 2021 +0200 +++ b/src/Pure/conv.ML Thu Sep 09 15:45:27 2021 +0200 @@ -81,7 +81,7 @@ fun try_conv cv = cv else_conv all_conv; fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; -fun cache_conv (cv: conv) = Thm.cterm_cache cv; +fun cache_conv (cv: conv) = Ctermtab.cterm_cache cv;