--- a/Nominal/nominal_dt_quot.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_dt_quot.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -82,7 +82,7 @@
     val _ = if is_Const rhs then () else warning "The definiens is not a constant"
 
   in
-    Quotient_Def.add_quotient_def (((binding, mx), Attrib.empty_binding), (lhs, rhs)) rsp_thm  ctxt
+    Quotient_Def.add_quotient_def (((binding, mx), Binding.empty_atts), (lhs, rhs)) rsp_thm  ctxt
   end