src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 44926 de3ed037c9a5
parent 44852 8ac91e7b6024
child 45002 df36896aae0f
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 14 06:49:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Sep 14 10:24:22 2011 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
     1.5          val _ = File.write main_file main
     1.6          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
     1.7 -        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls " ^
     1.8 +        val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
     1.9            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.10            " -o " ^ executable ^ ";"
    1.11          val (result, compilation_time) =