diff -r dec96cb3fbe0 -r 440fe0937b92 src/Doc/Tutorial/Rules/Basic.thy
--- a/src/Doc/Tutorial/Rules/Basic.thy	Sun May 28 08:07:40 2017 +0200
+++ b/src/Doc/Tutorial/Rules/Basic.thy	Sun May 28 11:32:15 2017 +0200
@@ -378,8 +378,8 @@
 
 (*both can be done by blast, which however hasn't been introduced yet*)
 lemma "[| P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k"
-apply (simp add: Least_def LeastM_def)
-by (blast intro: some_equality order_antisym)
+apply (simp add: Least_def)
+by (blast intro: order_antisym)
 
 theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
 apply (rule exI [of _  "\<lambda>x. SOME y. P x y"])