--- a/Nominal/Parser.thy	Thu Mar 11 10:39:29 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 11:15:14 2010 +0100
@@ -326,11 +326,11 @@
   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)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
 else
 let
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc
-    ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
+    (build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5) 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_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc