diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -63,12 +63,12 @@
 unfolding no_Check_in_def member_def by auto
 
 lemma [code_pred_def]: "feels_safe s r =
-(EX s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
+(EX s\<^sub>1 s\<^sub>2 s\<^sub>3 g c c'.
     s =
-    s\<^isub>3 @
-    [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 &
-    no_Check_in (s\<^isub>3 @ s\<^isub>2) r &
-    (\<not> (\<exists> g'. isinp (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r g')))"
+    s\<^sub>3 @
+    [Enter g r c] @ s\<^sub>2 @ [Check_in g r c'] @ s\<^sub>1 &
+    no_Check_in (s\<^sub>3 @ s\<^sub>2) r &
+    (\<not> (\<exists> g'. isinp (s\<^sub>2 @ [Check_in g r c] @ s\<^sub>1) r g')))"
 unfolding feels_safe_def isinp_def by auto
 
 setup {* Code_Prolog.map_code_options (K