# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276867378 -7200
# Node ID 29532d69111cef532265aa697e1133c57060bab6
# Parent  fab7f09dda225648fd68166344ce50a44af9cadb
changes for partial-equivalence quotient package

diff -r fab7f09dda22 -r 29532d69111c Nominal/Lift.thy
--- 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;