# HG changeset patch
# User bulwahn
# Date 1292495466 -3600
# Node ID 0bdc6fac5f48e5fff5545a0fae418ece50117f0d
# Parent  ba1eac745c5a0cadbe823324a90f8d948c0e5e1f
reactivating nitpick in Mutabelle

diff -r ba1eac745c5a -r 0bdc6fac5f48 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Dec 16 09:40:15 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Dec 16 11:31:06 2010 +0100
@@ -27,9 +27,10 @@
 (*
 val sledgehammer_mtd : mtd
 *)
+val nitpick_mtd : mtd
+
 (*
 val refute_mtd : mtd
-val nitpick_mtd : mtd
 *)
 
 val freezeT : term -> term
@@ -186,67 +187,26 @@
 val refute_mtd = ("refute", invoke_refute)
 *)
 
-(*
-open Nitpick_Util
-open Nitpick_Rep
-open Nitpick_Nut
+(** nitpick **)
 
 fun invoke_nitpick thy t =
   let
     val ctxt = ProofContext.init_global thy
     val state = Proof.init ctxt
+    val (res, _) = Nitpick.pick_nits_in_term state
+      (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t
+    val _ = Output.urgent_message ("Nitpick: " ^ res)
   in
-    let
-      val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Isar.default_params thy []) false [] t
-      val _ = Output.urgent_message ("Nitpick: " ^ res)
-    in
-      case res of
-        "genuine" => GenuineCex
-      | "likely_genuine" => GenuineCex
-      | "potential" => PotentialCex
-      | "none" => NoCex
-      | "unknown" => Donno
-      | _ => Error
-    end
-    handle ARG (loc, details) =>
-           (error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ "."))
-         | BAD (loc, details) =>
-           (error ("Internal error (" ^ quote loc ^ "): " ^ details ^ "."))
-         | LIMIT (_, details) =>
-           (warning ("Limit reached: " ^ details ^ "."); Donno)
-         | NOT_SUPPORTED details =>
-           (warning ("Unsupported case: " ^ details ^ "."); Donno)
-         | NUT (loc, us) =>
-           (error ("Invalid nut" ^ plural_s_for_list us ^
-                   " (" ^ quote loc ^ "): " ^
-                  commas (map (string_for_nut ctxt) us) ^ "."))
-         | REP (loc, Rs) =>
-           (error ("Invalid representation" ^ plural_s_for_list Rs ^
-                   " (" ^ quote loc ^ "): " ^
-                   commas (map string_for_rep Rs) ^ "."))
-         | TERM (loc, ts) =>
-           (error ("Invalid term" ^ plural_s_for_list ts ^
-                   " (" ^ quote loc ^ "): " ^
-                   commas (map (Syntax.string_of_term ctxt) ts) ^ "."))
-         | TYPE (loc, Ts, ts) =>
-           (error ("Invalid type" ^ plural_s_for_list Ts ^
-                   (if null ts then
-                      ""
-                    else
-                      " for term" ^ plural_s_for_list ts ^ " " ^
-                      commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
-                   " (" ^ quote loc ^ "): " ^
-                   commas (map (Syntax.string_of_typ ctxt) Ts) ^ "."))
-         | Kodkod.SYNTAX (_, details) =>
-           (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); Error)
-         | Refute.REFUTE (loc, details) =>
-           (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
-                   "."))
-         | Exn.Interrupt => raise Exn.Interrupt  (* FIXME violates Isabelle/ML exception model *)
-         | _ => (Output.urgent_message ("Unknown error in Nitpick"); Error)
+    rpair ([], NONE) (case res of
+      "genuine" => GenuineCex
+    | "likely_genuine" => GenuineCex
+    | "potential" => PotentialCex
+    | "none" => NoCex
+    | "unknown" => Donno
+    | _ => Error)
   end
+
 val nitpick_mtd = ("nitpick", invoke_nitpick)
-*)
 
 (* filtering forbidden theorems and mutants *)