--- a/Quot/quotient_def.ML	Mon Feb 15 14:51:17 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 14:58:03 2010 +0100
@@ -41,7 +41,7 @@
 let
   val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
   val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
-  val der_bname = Binding.name lhs_str
+  val derived_bname = Binding.name lhs_str
   val (qconst_bname, mx) =
     case bindmx of
       SOME (bname, mx) =>
@@ -50,9 +50,9 @@
             (quote lhs_str) ^ " differs from declaration " ^ (Binding.name_of bname) ^
             Position.str_of (Binding.pos_of bname))
         in
-          (der_bname, mx)
+          (derived_bname, mx)
         end
-      | NONE => (der_bname, NoSyn)
+      | NONE => (derived_bname, NoSyn)
   val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop