changeset 27865 | 27a8ad9612a3 |
parent 27239 | f2f42f9fa09d |
child 28174 | 626f0a79a4b9 |
--- a/src/HOL/Tools/meson.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Tools/meson.ML Thu Aug 14 16:52:46 2008 +0200 @@ -431,7 +431,7 @@ (*Use "theorem naming" to label the clauses*) fun name_thms label = let fun name1 (th, (k,ths)) = - (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths) + (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) in fn ths => #2 (foldr name1 (length ths, []) ths) end; (*Is the given disjunction an all-negative support clause?*)