src/HOL/Typerep.thy

--- a/src/HOL/Typerep.thy	Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Typerep.thy	Thu Jun 23 11:01:14 2016 +0200
@@ -58,7 +58,7 @@
     thy
     |> Class.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
+    |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;