# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1322661381 0
# Node ID 756f48abb40adff47c7ae4a281127cfb656e6b9f
# Parent  1afcbaf4242b9c7fceb8a051a58cd03b95dc3fe4
updated to changes in the quotient package (patch by Ondrej Kuncar)

diff -r 1afcbaf4242b -r 756f48abb40a Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Sun Nov 27 17:15:05 2011 +0000
+++ b/Nominal/nominal_dt_quot.ML	Wed Nov 30 13:56:21 2011 +0000
@@ -58,9 +58,10 @@
 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
   let
     val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
-    val qty_args2 = (qtys_descr ~~ qty_args1) ~~ alpha_equivp_thms
+    val qty_args2 = (map2 (fn descr => fn args1 => (descr, args1, NONE)) qtys_descr qty_args1)
+    val qty_args3 = qty_args2 ~~ alpha_equivp_thms
   in
-    fold_map Quotient_Type.add_quotient_type qty_args2 lthy
+    fold_map Quotient_Type.add_quotient_type qty_args3 lthy
   end