Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Typedef.thy
changeset 28083 103d9282a946
parent 27295 cfe5244301dd
child 28084 a05ca48ef263 
--- a/src/HOL/Typedef.thy	Tue Sep 02 14:10:32 2008 +0200
+++ b/src/HOL/Typedef.thy	Tue Sep 02 14:10:45 2008 +0200
@@ -145,7 +145,7 @@
     thy
     |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
+    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
     |> snd
     |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     |> LocalTheory.exit
isabelle