diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -67,8 +67,7 @@
    "ALL i :# M. P i"? 
 *)
 
-constdefs
-  msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b"
+definition msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" where
   "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
 
 syntax
@@ -214,8 +213,7 @@
   thus ?thesis by (simp add:multiset_eq_conv_count_eq)
 qed
 
-constdefs
-  multiset_prime_factorization :: "nat => nat multiset"
+definition multiset_prime_factorization :: "nat => nat multiset" where
   "multiset_prime_factorization n ==
      if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
        n = (PROD i :# M. i)))