--- a/Quot/Nominal/Perm.thy	Wed Feb 24 14:55:09 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 24 15:13:22 2010 +0100
@@ -9,9 +9,10 @@
 *}
 
 ML {*
-fun prove_perm_empty lthy induct perm_def perm_frees perm_indnames =
+fun prove_perm_empty lthy induct perm_def perm_frees =
 let
-  val perm_types = map fastype_of perm_frees
+  val perm_types = map fastype_of perm_frees;
+  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
   val gl =
     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
       (map (fn ((perm, T), x) => HOLogic.mk_eq
@@ -29,9 +30,34 @@
 end;
 *}
 
+ML {*
+fun prove_perm_append lthy induct perm_def perm_frees =
+let
+  val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
+  val pi1 = Free ("pi1", @{typ perm});
+  val pi2 = Free ("pi2", @{typ perm});
+  val perm_types = map fastype_of perm_frees
+  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  val gl =
+    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map (fn ((perm, T), x) =>
+          let
+            val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
+            val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
+          in HOLogic.mk_eq (lhs, rhs)
+          end)
+        (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
+  fun tac _ =
+    EVERY [
+      indtac induct perm_indnames 1,
+      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
+    ]
+in
+  split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac)
+end;
+*}
 
 ML {*
-
 (* TODO: full_name can be obtained from new_type_names with Datatype *)
 fun define_raw_perms new_type_names full_tnames thy =
 let
@@ -44,7 +70,6 @@
   val perm_types = map (fn (i, _) =>
     let val T = nth_dtyp i
     in @{typ perm} --> T --> T end) descr;
-  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
   val perm_names_types' = perm_names' ~~ perm_types;
   val pi = Free ("pi", @{typ perm});
   fun perm_eq_constr i (cname, dts) =
@@ -82,28 +107,11 @@
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
     val perm_frees =
       (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);
-    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees perm_indnames, length new_type_names);
-    val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
-    val pi1 = Free ("pi1", @{typ perm});
-    val pi2 = Free ("pi2", @{typ perm});
-    val perm_append_thms =
-       List.take ((split_conj_thm
-         (Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) []
-            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-               (map (fn ((perm, T), x) =>
-                   let
-                     val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
-                     val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
-                   in HOLogic.mk_eq (lhs, rhs)
-                   end)
-                 (perm_frees ~~
-                  map body_type perm_types ~~ perm_indnames))))
-            (fn _ => EVERY [indtac induct perm_indnames 1,
-               ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))),
-          length new_type_names);
+    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
+    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
     fun tac ctxt perm_thms =
       (Class.intro_classes_tac []) THEN (ALLGOALS (
-        simp_tac (@{simpset} addsimps perm_thms
+        simp_tac (HOL_ss addsimps perm_thms
       )));
     fun morphism phi = map (Morphism.thm phi);
   in