# HG changeset patch
# User blanchet
# Date 1410294529 -7200
# Node ID 87b59745dd6dd568d370a6ebe6599d40b9ddaf25
# Parent  10105897bc221085c6ce3f8165be9a0783496f0f
avoid internal fact

diff -r 10105897bc22 -r 87b59745dd6d src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Tue Sep 09 22:25:14 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Tue Sep 09 22:28:49 2014 +0200
@@ -206,7 +206,7 @@
   by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
 
 lemma A_prod_relprime: "gcd (setprod id A) p = 1"
-  by (metis DEADID.map_id all_A_relprime setprod_coprime_int)
+  by (metis id_def all_A_relprime setprod_coprime_int)
 
 
 subsection {* Relationships Between Gauss Sets *}