diff -r 88094aa77026 -r b12f0321dfb0 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Thu Dec 10 03:48:39 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 04:23:13 2009 +0100
@@ -84,7 +84,7 @@
   using c
 apply(induct xs)
 apply (metis Suc_neq_Zero card1_0)
-apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons)
+apply (metis FSet.card1_cons list_eq.intros(6) list_eq_refl mem_cons)
 done
 
 definition
@@ -107,7 +107,7 @@
   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
   apply (induct X)
   apply (simp)
-  apply (metis List.member.simps(1) QUOT_TYPE_I_fset.R_trans list_eq_refl mem_cons)
+  apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
   done
 
 quotient_def