--- a/Nominal/Lift.thy	Thu Jun 17 09:25:44 2010 +0200
+++ b/Nominal/Lift.thy	Fri Jun 18 15:22:58 2010 +0200
@@ -10,7 +10,7 @@
 fun define_quotient_types binds tys alphas equivps ctxt =
 let
   fun def_ty ((b, ty), (alpha, equivp)) ctxt =
-    Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha)), equivp) ctxt;
+    Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha, false)), equivp) ctxt;
   val alpha_equivps = List.take (equivps, length alphas)
   val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt;
   val quot_thms = map fst thms;