author | blanchet |
Fri, 30 Apr 2010 14:58:21 +0200 | |
changeset 36575 | 6e8a1c5eb0a8 |
parent 36574 | 870dfa6d00ce |
child 36578 | 663bb2bc1e72 |
child 36597 | fc184e0cc8bf |
--- 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