diff -r 93ab397f5980 -r 86c977b4a9bb Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Jun 01 15:01:05 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Jun 01 15:21:01 2010 +0200
@@ -403,11 +403,19 @@
  
   val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp
 
-  val (alpha_eqvt, lthy6a) =
+  
+
+  val (alpha_eqvt, _) =
     if get_STEPS lthy > 8
-    then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy_tmp'
+    then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp'
     else raise TEST lthy4
 
+  (*
+  val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt))
+  val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt))
+  val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt))
+  *)
+
   val _ = 
     if get_STEPS lthy > 9
     then true else raise TEST lthy4
@@ -417,15 +425,15 @@
 
   val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
 
-  val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a;
+  val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4;
   val alpha_equivp =
-    if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms
+    if !cheat_equivp then map (equivp_hack lthy4) alpha_trms
     else build_equivps alpha_trms reflps alpha_induct
-      inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy6a;
+      inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy6a;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>