diff -r 6e856be26ac7 -r 947e5f772a9c Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Thu Mar 11 11:41:27 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 12:26:24 2010 +0100
@@ -87,13 +87,18 @@
 *}
 
 ML {*
+  fun all_eqvts ctxt =
+    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
+  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
+
+ML {*
 fun constr_rsp_tac inj rsp equivps =
 let
   val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
 in
   REPEAT o rtac impI THEN'
-  simp_tac (HOL_ss addsimps inj) THEN'
-  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
+  simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW
   (asm_simp_tac HOL_ss THEN_ALL_NEW (
    rtac @{thm exI[of _ "0 :: perm"]} THEN'
    asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
@@ -134,7 +139,7 @@
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
+  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
   fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
@@ -153,11 +158,6 @@
 apply (rule_tac x="pi \<bullet> pia" in exI)
 by auto
 
-ML {*
-  fun all_eqvts ctxt =
-    Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
-  val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
 
 ML {*
 fun mk_minimal_ss ctxt =