src/HOL/Tools/Quotient/quotient_def.ML

   in
     error ("Head of quotient_definition " ^
       quote str ^ " differs from declaration " ^ name ^ pos)
   end
 
-fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
+fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy =
   let
     val (vars, ctxt) = prep_vars (the_list raw_var) lthy
     val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
     val lhs = prep_term T_opt ctxt lhs_raw
     val rhs = prep_term NONE ctxt rhs_raw

     val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
     val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
     val (_, prop') = Local_Defs.cert_def lthy prop
     val (_, newrhs) = Local_Defs.abs_def prop'
 
-    val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
+    val ((trm, (_ , thm)), lthy') =
+      Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
 
     (* data storage *)
     val qconst_data = {qconst = trm, rconst = rhs, def = thm}
 
     val lthy'' = lthy'