--- a/Nominal/NewParser.thy	Tue May 04 14:25:22 2010 +0100
+++ b/Nominal/NewParser.thy	Tue May 04 14:33:50 2010 +0100
@@ -382,12 +382,12 @@
   val distinct_thms = flat (map #distinct dtinfos);
   val rel_dtinfos = List.take (dtinfos, (length dts)); 
   val rel_distinct = map #distinct rel_dtinfos;  (* thm list list *)
-  val induct_thms = #induct dtinfo;
+  val induct_thm = #induct dtinfo;
   val exhaust_thms = map #exhaust dtinfos;
 
   (* definitions of raw permutations *)
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
-    if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts (length dts)) lthy1
+    if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
     else raise TEST lthy1
 
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
@@ -405,7 +405,7 @@
   val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
   val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls)
   val ((fv, fvbn), fv_def, lthy3a) = 
-    if STEPS > 3 then define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3
+    if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
     else raise TEST lthy3
   
 
@@ -432,8 +432,8 @@
 
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
-  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thms (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
-  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thms (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
+  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
+  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
@@ -442,7 +442,7 @@
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thms alpha_eq_iff_simp lthy6;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
     else build_equivps alpha_ts reflps alpha_induct
@@ -501,7 +501,7 @@
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = warning "Lifting induction";
   val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
-  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thms);
+  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
   fun note_simp_suffix s th ctxt =

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