--- a/Nominal/Rsp.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -86,10 +86,12 @@
   (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))))
 *}
 
+
 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)
+fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
+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 {*