1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jan 22 13:39:00 2010 +0100
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4        ("(3PROD _:#_. _)" [0, 51, 10] 10)
     1.5  
     1.6  translations
     1.7 -  "PROD i :# A. b" == "msetprod (%i. b) A"
     1.8 +  "PROD i :# A. b" == "CONST msetprod (%i. b) A"
     1.9  
    1.10  lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
    1.11    apply (simp add: msetprod_def power_add)