diff -r df3a952c6a67 -r 8728f7990f6d Nominal/Lift.thy
--- a/Nominal/Lift.thy	Wed Jun 23 15:21:04 2010 +0100
+++ b/Nominal/Lift.thy	Wed Jun 23 15:40:00 2010 +0100
@@ -9,7 +9,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;