diff -r 73c50e913db6 -r 31ba33a199c7 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Tue May 04 14:25:22 2010 +0100
+++ b/Nominal/Perm.thy	Tue May 04 14:33:50 2010 +0100
@@ -116,9 +116,8 @@
    user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_info : Datatype_Aux.info) user_dt_nos thy =
+fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
 let
-  val {descr as dt_descr, induct, sorts, ...} = dt_info;
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
   val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
 
@@ -138,8 +137,8 @@
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  val perm_zero_thms = prove_permute_zero lthy' induct perm_eq_thms perm_funs
-  val perm_plus_thms = prove_permute_plus lthy' induct perm_eq_thms perm_funs
+  val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
+  val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
   val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
   val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
   val perms_name = space_implode "_" perm_fn_names