--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Feb 22 19:31:00 2010 +0100
@@ -294,7 +294,8 @@
*)
]
-fun problem_for_nut ctxt name u =
+(* Proof.context -> string * nut -> Kodkod.problem *)
+fun problem_for_nut ctxt (name, u) =
let
val debug = false
val peephole_optim = true
@@ -320,15 +321,11 @@
formula = formula}
end
-(* string -> unit *)
-fun run_test name =
+(* unit -> unit *)
+fun run_all_tests () =
case Kodkod.solve_any_problem false NONE 0 1
- [problem_for_nut @{context} name
- (the (AList.lookup (op =) tests name))] of
+ (map (problem_for_nut @{context}) tests) of
Kodkod.Normal ([], _) => ()
- | _ => warning ("Test " ^ quote name ^ " failed")
-
-(* unit -> unit *)
-fun run_all_tests () = List.app run_test (map fst tests)
+ | _ => error "Tests failed"
end;