diff -r 4b0ad6c5d1ca -r 0a8a75e400da src/HOL/ex/Functions.thy
--- a/src/HOL/ex/Functions.thy	Thu Apr 28 11:34:26 2016 +0200
+++ b/src/HOL/ex/Functions.thy	Thu Apr 28 11:47:01 2016 +0200
@@ -125,8 +125,8 @@
 where
   "gcd3 x 0 = x"
 | "gcd3 0 y = y"
-| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
-| "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
+| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
+| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y"
   apply (case_tac x, case_tac a, auto)
   apply (case_tac ba, auto)
   done