--- a/FSet.thy	Fri Dec 04 15:04:05 2009 +0100
+++ b/FSet.thy	Fri Dec 04 15:18:33 2009 +0100
@@ -16,14 +16,14 @@
   shows "xs \<approx> xs"
   by (induct xs) (auto intro: list_eq.intros)
 
-lemma equiv_list_eq:
-  shows "EQUIV list_eq"
-  unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+lemma equivp_list_eq:
+  shows "equivp list_eq"
+  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
 quotient fset = "'a list" / "list_eq"
-  apply(rule equiv_list_eq)
+  apply(rule equivp_list_eq)
   done
 
 print_theorems
@@ -59,7 +59,7 @@
 term FUNION
 thm FUNION_def
 
-thm QUOTIENT_fset
+thm Quotient_fset
 
 thm QUOT_TYPE_I_fset.thm11
 
@@ -418,7 +418,7 @@
 done
 
 quotient fset2 = "'a list" / "list_eq"
-  apply(rule equiv_list_eq)
+  apply(rule equivp_list_eq)
   done
 
 quotient_def
@@ -431,7 +431,7 @@
 where
   "INSERT2 \<equiv> op #"
 
-ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
+ML {* val quot = @{thms Quotient_fset Quotient_fset2} *}
 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}