diff -r e4f40a0ea2e1 -r 02fbd0e7954a src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Library/GCD.thy	Mon Mar 17 18:37:05 2008 +0100
@@ -224,11 +224,11 @@
 definition
   lcm :: "nat \<times> nat \<Rightarrow> nat"
 where
-  "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
+  lcm_prim_def: "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
 
 lemma lcm_def:
   "lcm (m, n) = m * n div gcd (m, n)"
-  unfolding lcm_def by simp
+  unfolding lcm_prim_def by simp
 
 lemma prod_gcd_lcm:
   "m * n = gcd (m, n) * lcm (m, n)"