src/HOL/Typedef.thy

--- a/src/HOL/Typedef.thy	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/Typedef.thy	Thu Dec 04 14:43:33 2008 +0100
@@ -145,7 +145,7 @@
     thy
     |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
     |> `(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