--- a/Nominal-General/nominal_eqvt.ML	Wed May 12 16:57:01 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Wed May 12 16:33:50 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

--- a/Nominal/Ex/SingleLet.thy	Wed May 12 16:57:01 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Wed May 12 16:33:50 2010 +0100
@@ -31,7 +31,6 @@
 equivariance alpha_trm_raw
 
 
-
 end
 
 

--- a/Nominal/NewParser.thy	Wed May 12 16:57:01 2010 +0200
+++ b/Nominal/NewParser.thy	Wed May 12 16:33:50 2010 +0100
@@ -185,6 +185,8 @@
   | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
 *}
 
+ML {* print_depth 50 *}
+
 ML {*
 fun prep_bn dt_names dts eqs = 
 let
@@ -216,8 +218,9 @@
   val unordered = AList.group (op=) (map aux eqs)
   val unordered' = map (fn (x, y) =>  (x, AList.group (op=) y)) unordered
   val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
+  val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
 in
-  ordered
+  ordered'
 end
 *}
 
@@ -388,10 +391,9 @@
 
   (* definition of raw fv_functions *)
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
-  fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
-  val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
-  val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
-
+  fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
+  val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
+ 
   val (_, lthy2a) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
   val thy = Local_Theory.exit_global lthy2a;
@@ -401,10 +403,8 @@
   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
-  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp)
   val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls)
-  val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
-  
+   
   val ((fv, fvbn), fv_def, lthy3a) = 
     if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
     else raise TEST lthy3