diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -59,11 +59,11 @@
 
 declare List.member_rec[code_pred_def]
 
-lemma [code_pred_def]: "no_Check_in s r = (~ (EX g c. List.member s (Check_in g r c)))"
+lemma [code_pred_def]: "no_Check_in s r = (\<not> (\<exists>g c. List.member s (Check_in g r c)))"
 unfolding no_Check_in_def member_def by auto
 
 lemma [code_pred_def]: "feels_safe s r =
-(EX s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
+(\<exists>s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
     s =
     s\<^sub>3 @
     [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 &