# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1309363269 -3600
# Node ID b4404b13f7755831fbbf53131865ac964cdc4bcc
# Parent  06bf338e321575ced4dc6bb370f249863ff7b434
added a warning if a theorem is already declared as equivariant

diff -r 06bf338e3215 -r b4404b13f775 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Wed Jun 29 16:44:54 2011 +0100
+++ b/Nominal/Ex/Let.thy	Wed Jun 29 17:01:09 2011 +0100
@@ -129,12 +129,6 @@
 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)"
   by (simp add: permute_pure)
 
-(* TODO: should be provided by nominal *)
-lemmas [eqvt] = trm_assn.fv_bn_eqvt
-thm trm_assn.fv_bn_eqvt
-
-
-thm Abs_lst_fcb
 
 lemma Abs_lst_fcb2:
   fixes as bs :: "'a :: fs"
diff -r 06bf338e3215 -r b4404b13f775 Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Wed Jun 29 16:44:54 2011 +0100
+++ b/Nominal/nominal_thmdecls.ML	Wed Jun 29 17:01:09 2011 +0100
@@ -58,7 +58,13 @@
 val get_eqvts_thms = eqvts o  Context.Proof;
 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
 
-val add_thm = EqvtData.map o Item_Net.update;
+fun checked_update key net =
+  (if Item_Net.member net key then 
+     warning "Theorem already declared as equivariant."
+   else (); 
+   Item_Net.update key net)
+
+val add_thm = EqvtData.map o checked_update;
 val del_thm = EqvtData.map o Item_Net.remove;
 
 fun add_raw_thm thm =