--- a/Nominal/NewParser.thy	Sun Apr 25 07:54:28 2010 +0200
+++ b/Nominal/NewParser.thy	Sun Apr 25 08:06:43 2010 +0200
@@ -269,9 +269,14 @@
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
-  val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy2) =
+  val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
     raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 
+  val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
+  val {descr, sorts, ...} = dtinfo;
+
+  val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
+    Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
 in
   ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2)
 end
@@ -490,9 +495,12 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = {atom x}"
 
+
 typ exp_raw 
 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
+thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
+