src/HOL/Typerep.thy
changeset 63352 4eaf35781b23
parent 63180 ddfd021884b4
child 66330 dcb3e6bdc00a
     1.1 --- a/src/HOL/Typerep.thy	Wed Jun 22 16:04:03 2016 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Thu Jun 23 11:01:14 2016 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4      thy
     1.5      |> Class.instantiation ([tyco], vs, @{sort typerep})
     1.6      |> `(fn lthy => Syntax.check_term lthy eq)
     1.7 -    |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
     1.8 +    |-> (fn eq => Specification.definition NONE [] [] (Binding.empty_atts, eq))
     1.9      |> snd
    1.10      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    1.11    end;