src/HOL/Tools/Nitpick/nitpick_tests.ML
changeset 35284 9edc2bd6d2bd
parent 35280 54ab4921f826
child 35333 f61de25f71f9
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 22 14:36:10 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 22 19:31:00 2010 +0100
     1.3 @@ -294,7 +294,8 @@
     1.4  *)
     1.5    ]
     1.6  
     1.7 -fun problem_for_nut ctxt name u =
     1.8 +(* Proof.context -> string * nut -> Kodkod.problem *)
     1.9 +fun problem_for_nut ctxt (name, u) =
    1.10    let
    1.11      val debug = false
    1.12      val peephole_optim = true
    1.13 @@ -320,15 +321,11 @@
    1.14       formula = formula}
    1.15    end
    1.16  
    1.17 -(* string -> unit *)
    1.18 -fun run_test name =
    1.19 +(* unit -> unit *)
    1.20 +fun run_all_tests () =
    1.21    case Kodkod.solve_any_problem false NONE 0 1
    1.22 -           [problem_for_nut @{context} name
    1.23 -                            (the (AList.lookup (op =) tests name))] of
    1.24 +                                (map (problem_for_nut @{context}) tests) of
    1.25      Kodkod.Normal ([], _) => ()
    1.26 -  | _ => warning ("Test " ^ quote name ^ " failed")
    1.27 -
    1.28 -(* unit -> unit *)
    1.29 -fun run_all_tests () = List.app run_test (map fst tests)
    1.30 +  | _ => error "Tests failed"
    1.31  
    1.32  end;