diff -r 381b391351b5 -r a05d0c1b0cb3 src/HOL/Extraction/Euclid.thy
--- a/src/HOL/Extraction/Euclid.thy	Fri Jun 04 17:32:30 2010 +0200
+++ b/src/HOL/Extraction/Euclid.thy	Fri Jun 04 19:36:40 2010 +0200
@@ -153,7 +153,7 @@
   assumes "all_prime ps" and "ps \<noteq> []"
   shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)"
   using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
-    (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult  del: One_nat_def)
+    (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
 
 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)"
 proof (induct n rule: nat_wf_ind)