--- a/QuotMain.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -141,12 +141,12 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
-declare [[map list = (map, LIST_REL)]]
+declare [[map list = (map, list_rel)]]
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
 
-lemmas [quotient_thm] = 
-  FUN_Quotient LIST_Quotient
+lemmas [quotient_thm] =
+  fun_quotient list_quotient
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
@@ -214,7 +214,7 @@
   done
 
 lemmas id_simps =
-  FUN_MAP_I[THEN eq_reflection]
+  fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
   prod_fun_id map_id
@@ -610,7 +610,7 @@
     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
     val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
-    (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)
+    (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs
   in
   ObjectLogic.full_atomize_tac THEN'