diff -r 93dce7c71929 -r d705d7ae2410 Quot/quotient.ML
--- a/Quot/quotient.ML	Fri Dec 11 19:19:50 2009 +0100
+++ b/Quot/quotient.ML	Fri Dec 11 19:22:30 2009 +0100
@@ -132,12 +132,12 @@
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
   (* ABS and REP definitions *)
-  val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
-  val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
+  val ABS_const = Const (@{const_name "QUOT_TYPE.abs"}, dummyT )
+  val REP_const = Const (@{const_name "QUOT_TYPE.rep"}, dummyT )
   val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
   val REP_trm = Syntax.check_term lthy1 (REP_const $ rep)
-  val ABS_name = Binding.prefix_name "ABS_" qty_name
-  val REP_name = Binding.prefix_name "REP_" qty_name
+  val ABS_name = Binding.prefix_name "abs_" qty_name
+  val REP_name = Binding.prefix_name "rep_" qty_name
   val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
          lthy1 |> define (ABS_name, NoSyn, ABS_trm)
                ||>> define (REP_name, NoSyn, REP_trm)