diff -r 050104f01bf9 -r 80a1aa30e24d src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -533,8 +533,8 @@
 of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
 explosions.\<close>
 
-lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
+lemmas (in linordered_field) sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
+lemmas sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
 
 
 instantiation rat :: distrib_lattice