--- a/Nominal/Parser.thy	Tue Mar 02 21:10:04 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 02 21:43:27 2010 +0100
@@ -231,7 +231,7 @@
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3;
-  val alpha_ts_loc = #preds alpha
+(*  val alpha_ts_loc = #preds alpha
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
   val alpha_induct_loc = #induct alpha
@@ -254,9 +254,9 @@
   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), lthy7)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 end
 *}