src/HOL/Typerep.thy
changeset 28965 1de908189869
parent 28952 15a4b2cf8c34
child 29574 5897b2688ccc
     1.1 --- a/src/HOL/Typerep.thy	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/HOL/Typerep.thy	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4      thy
     1.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
     1.6      |> `(fn lthy => Syntax.check_term lthy eq)
     1.7 -    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     1.8 +    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     1.9      |> snd
    1.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.11      |> LocalTheory.exit_global