changeset 70545 | b93ba98e627a |
parent 67721 | 5348bea4accd |
child 74525 | c960bfcb91db |
--- a/src/Pure/Tools/find_theorems.ML Fri Aug 16 10:20:41 2019 +0200 +++ b/src/Pure/Tools/find_theorems.ML Fri Aug 16 10:33:25 2019 +0200 @@ -125,7 +125,7 @@ (* filter_name *) fun filter_name str_pat (thmref, _) = - if match_string str_pat (Facts.name_of_ref thmref) + if match_string str_pat (Facts.ref_name thmref) then SOME (0, 0, 0) else NONE;