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