diff -r 872187804ff5 -r b3a5bda07007 Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Wed May 12 15:17:35 2010 +0100
+++ b/Nominal-General/nominal_eqvt.ML	Wed May 12 16:26:06 2010 +0100
@@ -149,6 +149,12 @@
 
 fun equivariance pred_trms raw_induct intrs ctxt = 
 let
+  val is_already_eqvt = 
+    filter (is_eqvt ctxt) pred_trms
+    |> map (Syntax.string_of_term ctxt)
+  val _ = if null is_already_eqvt then ()
+    else error ("Already equivariant: " ^ commas is_already_eqvt)
+
   val pred_names = map (fst o dest_Const) pred_trms
   val raw_induct' = atomize_induct ctxt raw_induct
   val intrs' = map atomize_intr intrs