src/HOL/Library/code_test.ML
changeset 59323 468bd3aedfa1
parent 58832 ec9550bd5fd7
child 59720 f893472fff31
     1.1 --- a/src/HOL/Library/code_test.ML	Thu Jan 08 18:23:29 2015 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Fri Jan 09 08:36:59 2015 +0100
     1.3 @@ -571,16 +571,15 @@
     1.4      "compile test cases to target languages, execute them and report results"
     1.5        (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
     1.6  
     1.7 -val _ = Context.>> (Context.map_theory (
     1.8 -  fold add_driver
     1.9 -    [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
    1.10 -     (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
    1.11 -     (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
    1.12 -     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
    1.13 -     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
    1.14 -     (scalaN, (evaluate_in_scala, Code_Scala.target))]
    1.15 -    #> fold (fn target => Value.add_evaluator (target, eval_term target))
    1.16 -      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]
    1.17 -    ))
    1.18 +val _ = Theory.setup (fold add_driver
    1.19 +  [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
    1.20 +   (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
    1.21 +   (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
    1.22 +   (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
    1.23 +   (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
    1.24 +   (scalaN, (evaluate_in_scala, Code_Scala.target))]
    1.25 +  #> fold (fn target => Value.add_evaluator (target, eval_term target))
    1.26 +    [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]);
    1.27 +
    1.28  end
    1.29