# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271666108 -7200
# Node ID 7af807a85e226fa822e8d089c99f4e23516448ca
# Parent  b2efe803f1da5a1ad5f2a06590a13f930db4d23e
Accept non-equality eqvt rules in support proofs.

diff -r b2efe803f1da -r 7af807a85e22 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon Apr 19 10:00:52 2010 +0200
+++ b/Nominal/Rsp.thy	Mon Apr 19 10:35:08 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
 *}