# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272949513 -3600
# Node ID be512c15daa5edfb86a4001ecf71be28ca3116d0
# Parent  3622cae9b10ea0629d22e7ad0a704be640eac275
tuned

diff -r 3622cae9b10e -r be512c15daa5 Nominal/Perm.thy
--- 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);