1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 31 10:29:04 2010 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 31 17:20:41 2010 +0200
1.3 @@ -316,10 +316,6 @@
1.4 error ("Invalid term" ^ plural_s_for_list ts ^
1.5 " (" ^ quote loc ^ "): " ^
1.6 commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
1.7 - | TOO_LARGE (_, details) =>
1.8 - (warning ("Limit reached: " ^ details ^ "."); x)
1.9 - | TOO_SMALL (_, details) =>
1.10 - (warning ("Limit reached: " ^ details ^ "."); x)
1.11 | TYPE (loc, Ts, ts) =>
1.12 error ("Invalid type" ^ plural_s_for_list Ts ^
1.13 (if null ts then
1.14 @@ -329,8 +325,6 @@
1.15 commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
1.16 " (" ^ quote loc ^ "): " ^
1.17 commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
1.18 - | Kodkod.SYNTAX (_, details) =>
1.19 - (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
1.20 | Refute.REFUTE (loc, details) =>
1.21 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
1.22