--- a/Nominal/Parser.thy	Thu Mar 04 11:16:36 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 04 12:00:11 2010 +0100
@@ -248,15 +248,15 @@
   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;
   val lthy7 = define_quotient_type
     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts))
-    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;*)
+    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy7)
 end
 *}