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/Pure/display.ML
changeset 20076 def4ad161528
parent 19806 f860b7a98445
child 20211 c7f907f41f7c 
--- a/src/Pure/display.ML	Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/display.ML	Tue Jul 11 12:17:01 2006 +0200
@@ -191,7 +191,7 @@
     val tfrees = map (fn v => TFree (v, []));
     fun pretty_type syn (t, (Type.LogicalType n, _)) =
           if syn then NONE
-          else SOME (prt_typ (Type (t, tfrees (Term.invent_names [] "'a" n))))
+          else SOME (prt_typ (Type (t, tfrees (Name.invent_list [] "'a" n))))
       | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
isabelle