src/HOL/Tools/meson.ML
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?*)