# HG changeset patch
# User nipkow
# Date 1345033602 -7200
# Node ID 21d4ed91912fd0d1830621729cda8cc69d822c0f
# Parent  6f0699239bc30f41520c619cbe0612c5feeeb5ea
fixed proof

diff -r 6f0699239bc3 -r 21d4ed91912f src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Aug 15 14:00:12 2012 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Aug 15 14:26:42 2012 +0200
@@ -544,12 +544,7 @@
   apply (erule ssubst)
   apply (subst setprod_Un_disjoint)
   apply auto
-  apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = 
-      (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
-  apply (erule ssubst)
-  apply (simp add: setprod_1)
-  apply (erule prime_factorization_nat)
-  apply (rule setprod_cong, auto)
+  apply(simp add: prime_factorization_nat)
   apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
       (prime_factors k - prime_factors l)")
   apply (erule ssubst)
@@ -557,9 +552,7 @@
   apply auto
   apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
       (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
-  apply (erule ssubst)
-  apply (simp add: setprod_1)
-  apply (erule prime_factorization_nat)
+  apply (simp add: prime_factorization_nat)
   apply (rule setprod_cong, auto)
   done