--- a/Nominal/nominal_dt_rawfuns.ML	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Dec 15 16:20:42 2011 +0000
@@ -94,7 +94,7 @@
   fun cntrs_order ((bn, dt_index), data) = 
   let
     val dt = nth dts dt_index                      
-    val cts = (fn (_, _, _, x) => x) dt     
+    val cts = snd dt     
     val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts  
   in
     (bn, (bn, dt_index, order (op=) ct_names data))