# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1273677966 -3600
# Node ID b3a5bda07007b0d9178238a078303a3b4c085267
# Parent  872187804ff57e74a8c0cfc7a975f801b44361c3
added a test whether some of the constants already equivariant (then the procedure has to fail).

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