diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -11,7 +11,7 @@
 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
 by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
 
-lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
+lemma [code_pred_inline]: "(-) == (%A B x. A x \<and> \<not> B x)"
 by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
 *)