src/HOL/Typedef.thy
changeset 28965 1de908189869
parent 28394 b9c8e3a12a98
child 29056 dc08e3990c77
     1.1 --- a/src/HOL/Typedef.thy	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/HOL/Typedef.thy	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4      thy
     1.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
     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