--- a/Nominal/Parser.thy	Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Parser.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -456,9 +456,12 @@
   val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
-  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff
-  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1
-  val q_eq_iff_pre1 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
+  val _ = map tracing (map PolyML.makestring alpha_eq_iff);
+  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
+  val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
+  val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
+  val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
+  val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;