--- a/Nominal/NewParser.thy	Tue Jul 27 23:34:30 2010 +0200
+++ b/Nominal/NewParser.thy	Thu Jul 29 10:16:33 2010 +0100
@@ -362,7 +362,7 @@
   (* definition of alpha_eq_iff  lemmas *)
   (* they have a funny shape for the simplifier *)
   val _ = warning "Eq-iff theorems";
-  val alpha_eq_iff = 
+  val (alpha_eq_iff_simps, alpha_eq_iff) = 
     if get_STEPS lthy > 5
     then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
     else raise TEST lthy4
@@ -426,7 +426,9 @@
   (* auxiliary lemmas for respectfulness proofs *)
   (* HERE *)
   
-
+  val test = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs raw_bns raw_fv_bns
+    alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+  val _ = tracing ("goals\n" ^ cat_lines (map (Syntax.string_of_term lthy6 o prop_of) test))
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -481,7 +483,8 @@
 
   val (_, lthy8') = lthy8
      |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
-     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) 
+     ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
+     ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) 
      ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) 
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws)