--- a/Quot/Nominal/Perm.thy	Wed Feb 24 14:37:51 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 24 14:55:09 2010 +0100
@@ -9,6 +9,28 @@
 *}
 
 ML {*
+fun prove_perm_empty lthy induct perm_def perm_frees perm_indnames =
+let
+  val perm_types = map fastype_of perm_frees
+  val gl =
+    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map (fn ((perm, T), x) => HOLogic.mk_eq
+          (perm $ @{term "0 :: perm"} $ Free (x, T),
+           Free (x, T)))
+       (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_zero} :: perm_def)))
+    ];
+in
+  split_conj_thm (Goal.prove lthy 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 =
@@ -60,23 +82,7 @@
         (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 =
-      let
-        val gl =
-          HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-            (map (fn ((perm, T), x) => HOLogic.mk_eq
-                (perm $ @{term "0 :: perm"} $ Free (x, T),
-                 Free (x, T)))
-             (perm_frees ~~
-              map body_type perm_types ~~ perm_indnames)));
-        fun tac {context = ctxt, ...} =
-          EVERY [
-            indtac induct perm_indnames 1,
-            ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))
-          ];
-      in
-        (List.take (split_conj_thm (Goal.prove lthy' perm_indnames [] gl tac), length new_type_names))
-      end;
+    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});