--- a/Nominal/Parser.thy	Tue Mar 16 18:19:00 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 16 20:07:13 2010 +0100
@@ -337,14 +337,22 @@
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
+  val _ = tracing "3";
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
     else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5
+  val _ = tracing "4";
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5;
-  val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
+  val _ = tracing "4a";
+  val (fv_bn_eqvts, lthy6a) = 
+    if fv_ts_loc_bn = [] then ([], lthy6) else
+    fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) 
+      (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
+  val _ = tracing "4b";
   val lthy6 = lthy6a;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
+  val _ = tracing "5";
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1