--- a/Nominal/Parser.thy	Wed Mar 10 16:59:08 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 10:10:23 2010 +0100
@@ -319,7 +319,7 @@
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 in
 if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
+  ((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;
@@ -327,8 +327,8 @@
     ((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;
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
-    (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
+  fun alpha_eqvt_tac' _ = alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy6 1
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms alpha_eqvt_tac' lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
   val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc