src/HOL/Typedef.thy
changeset 28083 103d9282a946
parent 27295 cfe5244301dd
child 28084 a05ca48ef263
     1.1 --- a/src/HOL/Typedef.thy	Tue Sep 02 14:10:32 2008 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Tue Sep 02 14:10:45 2008 +0200
     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, (("", []), eq)))
     1.8 +    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
     1.9      |> snd
    1.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.11      |> LocalTheory.exit