src/HOL/Algebra/FiniteProduct.thy

--- a/src/HOL/Algebra/FiniteProduct.thy	Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Oct 07 16:07:50 2008 +0200
@@ -291,7 +291,7 @@
   finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
   "finprod G f A == if finite A
       then foldD (carrier G) (mult G o f) \<one> A
-      else arbitrary"
+      else undefined"
 
 syntax
   "_finprod" :: "index => idt => 'a set => 'b => 'b"