--- a/Nominal/Rsp.thy	Mon Apr 19 09:25:31 2010 +0200
+++ b/Nominal/Rsp.thy	Mon Apr 19 09:27:53 2010 +0200
@@ -70,7 +70,7 @@
 *}
 
 ML {*
-fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
+fun sym_eqvts ctxt = maps (fn x => [sym OF [x]] handle _ => []) (Nominal_ThmDecls.get_eqvts_thms ctxt)
 fun all_eqvts ctxt =
   Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
 *}