diff -r ade2f8fcf8e8 -r 51ef8a3cb6ef Nominal/nominal_dt_rawfuns.ML --- 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))