# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266240483 -3600
# Node ID b5b386502a8a7bde88791824b802ff3337b5d28f
# Parent  2e5303b7dde408db94bbfc0e473e14e8f0302d9b
Finished introducing the binding.

diff -r 2e5303b7dde4 -r b5b386502a8a Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Mon Feb 15 13:40:03 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 14:28:03 2010 +0100
@@ -7,10 +7,10 @@
 
 signature QUOTIENT_DEF =
 sig
-  val quotient_def: (Attrib.binding * mixfix) option * (Attrib.binding * (term * term)) ->
+  val quotient_def: (binding * mixfix) option * (Attrib.binding * (term * term)) ->
     local_theory -> (term * thm) * local_theory
 
-  val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) ->
+  val quotdef_cmd: (binding * mixfix) option * (Attrib.binding * (string * string)) ->
     local_theory -> (term * thm) * local_theory
 end;
 
@@ -39,14 +39,20 @@
 *)
 fun quotient_def (bindmx, (attr, (lhs, rhs))) lthy =
 let
-  val mx =
-    case bindmx of
-      SOME (_, mx) => mx
-    | _ => NoSyn
   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 qconst_bname = Binding.name lhs_str
+  val der_bname = Binding.name lhs_str
+  val (qconst_bname, mx) =
+    case bindmx of
+      SOME (bname, mx) =>
+        let
+          val _ = (Name.of_binding bname = lhs_str) orelse error ("Head of quotient_definition " ^ 
+            (quote lhs_str) ^ " differs from declaration " ^ (Binding.name_of bname) ^
+            Position.str_of (Binding.pos_of bname))
+        in
+          (der_bname, mx)
+        end
+      | NONE => (der_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