--- a/Nominal-General/nominal_permeq.ML	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Fri Apr 16 16:29:11 2010 +0200
@@ -106,11 +106,16 @@
 
 (* conversion that raises an error or prints a warning message, 
    if a permutation on a constant or application cannot be analysed *)
-fun progress_info_conv ctxt strict_flag ctrm =
+fun progress_info_conv ctxt strict_flag bad_hds ctrm =
 let
-  fun msg trm = 
-    (if strict_flag then error else warning) 
-      ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+  fun msg trm =
+    let
+      val hd = head_of trm 
+    in 
+    if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
+    else (if strict_flag then error else warning) 
+           ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+    end
 
   val _ = case (term_of ctrm) of
       Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
@@ -136,7 +141,7 @@
       eqvt_apply_conv bad_hds,
       eqvt_lambda_conv,
       More_Conv.rewrs_conv post_thms,
-      progress_info_conv ctxt strict_flag
+      progress_info_conv ctxt strict_flag bad_hds
     ] ctrm
 end