--- a/src/HOL/SMT_Examples/SMT_Examples.thy Mon Apr 09 17:21:10 2018 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Wed Apr 11 10:59:13 2018 +0200
@@ -396,7 +396,7 @@
False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
by smt
-lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by smt
+lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by (smt int_nat_eq)
definition prime_nat :: "nat \<Rightarrow> bool" where
"prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"