Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorChristian Urban <urbanc@in.tum.de>
Tue, 04 May 2010 06:05:13 +0100
changeset 2036 be512c15daa5
parent 2035 3622cae9b10e
child 2037 205ac2d13339
tuned
Nominal/Perm.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Perm.thy	Tue May 04 06:02:45 2010 +0100
+++ b/Nominal/Perm.thy	Tue May 04 06:05:13 2010 +0100
@@ -119,7 +119,7 @@
 fun define_raw_perms (dt_info : Datatype_Aux.info) thy =
 let
   val {descr as dt_descr, induct, sorts, ...} = dt_info;
-  val dt_nos = length descr
+  val dt_nos = length dt_descr
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
   val full_tnames = List.take (all_full_tnames, dt_nos);
nominal2