--- a/quotient.ML	Fri Dec 04 15:04:05 2009 +0100
+++ b/quotient.ML	Fri Dec 04 15:18:33 2009 +0100
@@ -102,13 +102,13 @@
 (* proves the quotient theorem *)
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
-  val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
+  val quotient_const = Const (@{const_name "Quotient"}, dummyT)
   val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
              |> Syntax.check_term lthy
 
   val typedef_quotient_thm_tac =
     EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
-            rtac @{thm QUOT_TYPE.QUOTIENT},
+            rtac @{thm QUOT_TYPE.Quotient},
             rtac quot_type_thm]
 in
   Goal.prove lthy [] [] goal
@@ -146,7 +146,7 @@
 
   (* quotient theorem *)
   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
-  val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
+  val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
 
   (* storing the quot-info *)
   val qty_str = fst (Term.dest_Type abs_ty)
@@ -157,7 +157,7 @@
   (* FIXME: to recalculated in for example REGULARIZE *)
 
   (* storing of the equiv_thm under a name *)
-  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3
+  val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -205,9 +205,9 @@
 let
   fun mk_goal (rty, rel) =
   let
-    val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+    val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   in 
-    HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel)
+    HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
   end
 
   val goals = map (mk_goal o snd) quot_list