--- a/Nominal/Rsp.thy	Tue Mar 02 15:13:00 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 17:11:19 2010 +0100
@@ -132,7 +132,7 @@
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
   fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW
     (asm_full_simp_tac (HOL_ss addsimps
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
   val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
   val thms = HOLogic.conj_elims thm
 in
@@ -161,14 +161,14 @@
   fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   (
    (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
+      ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))
     THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN'
       REPEAT o etac conjE THEN'
       (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW
       (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
       (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW
     (asm_full_simp_tac (HOL_ss addsimps 
-      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1
+      ((Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps))))) 1
   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)