diff -r 3f227ed7e3e5 -r cb03b34340e9 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Feb 01 11:16:13 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Feb 01 11:16:31 2010 +0100
@@ -186,13 +186,14 @@
   using a b c
   by (lifting int_induct_raw)
 
-lemma ex1tst: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
+lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
 sorry
 
-lemma ex1tst': "\<exists>! (x :: my_int). x = x"
+lemma ex1tst': "\<exists>!(x::my_int). x = x"
 apply(lifting ex1tst)
 done
 
+
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
 done