changeset 36575 | 6e8a1c5eb0a8 |
parent 36555 | 8ff45c2076da |
child 37213 | efcad7594872 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Apr 30 14:52:49 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Apr 30 14:58:21 2010 +0200 @@ -1393,7 +1393,7 @@ cons (T', monomorphic_term (Sign.typ_match thy (T', T) Vartab.empty) t) handle Type.TYPE_MATCH => I - | Refute.REFUTE _ => + | TERM _ => if slack then I else