1.1 --- a/src/HOL/Tools/meson.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -390,8 +390,7 @@
     1.4  (*Use "theorem naming" to label the clauses*)
     1.5  fun name_thms label =
     1.6      let fun name1 (th, (k,ths)) =
     1.7 -	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
     1.8 -
     1.9 +	  (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
    1.10      in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    1.11  
    1.12  (*Is the given disjunction an all-negative support clause?*)