diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/ex/While_Combinator_Example.thy
--- a/src/HOL/ex/While_Combinator_Example.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/ex/While_Combinator_Example.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -17,7 +17,7 @@
     lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
 apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
                 r = "((Pow U \<times> UNIV) \<times> (Pow U \<times> UNIV)) \<inter>
-                     inv_image finite_psubset (op - U o fst)" in while_rule)
+                     inv_image finite_psubset ((-) U o fst)" in while_rule)
    apply (subst lfp_unfold)
     apply assumption
    apply (simp add: monoD)