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