src/HOL/GCD.thy

--- a/src/HOL/GCD.thy	Fri Jul 27 19:27:21 2012 +0200
+++ b/src/HOL/GCD.thy	Fri Jul 27 19:57:23 2012 +0200
@@ -610,8 +610,8 @@
   apply (erule subst)
   apply (rule iffI)
   apply force
-  apply (drule_tac x = "abs e" in exI)
-  apply (case_tac "e >= 0")
+  apply (drule_tac x = "abs ?e" in exI)
+  apply (case_tac "(?e::int) >= 0")
   apply force
   apply force
 done