src/HOL/Tools/Nitpick/nitpick_isar.ML
changeset 37211 efcad7594872
parent 37163 f69efa106feb
child 37259 dde817e6dfb1
     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