# HG changeset patch
# User huffman
# Date 1245375074 25200
# Node ID d1f7b6245a754ea508d47ea284b46c4cd3de5b45
# Parent  32f07b47f9c548c237f7d1ac979ed7496250a90c
fix name clash with old/new prime libraries

diff -r 32f07b47f9c5 -r d1f7b6245a75 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Thu Jun 18 12:00:03 2009 -0700
+++ b/src/HOL/Algebra/Exponent.thy	Thu Jun 18 18:31:14 2009 -0700
@@ -9,6 +9,8 @@
 imports Main Primes Binomial
 begin
 
+hide (open) const GCD.gcd GCD.coprime GCD.prime
+
 section {*Sylow's Theorem*}
 
 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}