Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.

--- a/src/HOL/GCD.thy	Sun Jul 12 14:48:01 2009 +0200
+++ b/src/HOL/GCD.thy	Mon Jul 13 19:07:05 2009 +0200
@@ -1503,7 +1503,7 @@
 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
 
 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
-by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff)
+by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
 
 
 subsection {* Primes *}