diff -r b452e11e409f -r 25b02cc185e2 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 10:22:24 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 10:39:29 2010 +0100
@@ -323,13 +323,13 @@
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
   val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
+  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 in
 if !restricted_nominal = 0 then
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 else
 let
-  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
-  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
   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;