1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Apr 14 23:34:18 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,28 +0,0 @@
     1.4 -(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
     1.5 -    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     1.6 -*)
     1.7 -
     1.8 -structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
     1.9 -struct
    1.10 -
    1.11 -fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: "
    1.12 -
    1.13 -fun init _ = I
    1.14 -fun done _ _ = ()
    1.15 -
    1.16 -fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
    1.17 -  let
    1.18 -    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
    1.19 -    val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
    1.20 -  in
    1.21 -    (case TimeLimit.timeLimit timeout quickcheck pre of
    1.22 -      NONE => log (qc_tag id ^ "no counterexample")
    1.23 -    | SOME _ => log (qc_tag id ^ "counterexample found"))
    1.24 -  end
    1.25 -  handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
    1.26 -       | ERROR msg => log (qc_tag id ^ "error: " ^ msg)
    1.27 -
    1.28 -fun invoke args =
    1.29 -  Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done)
    1.30 -
    1.31 -end