--- a/Nominal/Parser.thy	Wed Mar 03 12:48:05 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 03 14:22:58 2010 +0100
@@ -245,10 +245,10 @@
   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
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
-(*  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms 
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
     (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
-  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
+(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_names = map (fn (_, b, _, _) => b) dts;