--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 12:20:08 2010 +0200
@@ -715,7 +715,7 @@
val thy = ProofContext.theory_of ctxt
val (x as (_, T)) = (s, unarize_unbox_etc_type T)
in
- Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
+ is_real_constr thy x orelse is_record_constr x orelse
(is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
is_coconstr thy x
end
@@ -861,9 +861,9 @@
let
val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
in
- map (fn (s', Us) =>
- (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
- ---> T)) constrs
+ map (apsnd (fn Us =>
+ map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+ constrs
end
| NONE =>
if is_record_type T then