# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266242283 -3600
# Node ID 64d896cc16f8d8f837a5b521cbfc8a750262f567
# Parent  389d81959922467bee4ac42d3c12303322f482ca
der_bname -> derived_bname

diff -r 389d81959922 -r 64d896cc16f8 Quot/quotient_def.ML
--- 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