
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);
 




