# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1363019445 0
# Node ID 024d07886de86a5b9e01f9cde6688fa312b8a3e7
# Parent  d3f7c8cce53b0652c5e59d68e6fa001e464c412d
updated to quotient package changes (by Kuncar)

diff -r d3f7c8cce53b -r 024d07886de8 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Tue Feb 19 05:42:51 2013 +0000
+++ b/Nominal/nominal_dt_quot.ML	Mon Mar 11 16:30:45 2013 +0000
@@ -58,7 +58,7 @@
 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 = (map2 (fn descr => fn args1 => (descr, args1, (NONE, false))) qtys_descr qty_args1)
+    val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, false, NONE))) qtys_descr qty_args1
     val qty_args3 = qty_args2 ~~ alpha_equivp_thms
   in
     fold_map Quotient_Type.add_quotient_type qty_args3 lthy