diff -r 20ee31bc34d5 -r d134bd4f6d1b Nominal/nominal_dt_rawperm.ML
--- a/Nominal/nominal_dt_rawperm.ML	Fri May 21 00:44:39 2010 +0100
+++ b/Nominal/nominal_dt_rawperm.ML	Fri May 21 05:58:23 2010 +0100
@@ -103,7 +103,7 @@
 (* user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_descr:Datatype.descr) sorts induct_thm user_dt_nos thy =
+fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
 let
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
   val user_full_tnames = List.take (all_full_tnames, user_dt_nos);