src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 48270 9cfd3e7ad5c8
parent 47843 4da917ed49b7
child 48272 db75b4005d9a
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 16 11:26:16 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 16 15:55:21 2012 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    val allow_existentials : bool Config.T
     1.5    val finite_functions : bool Config.T
     1.6    val overlord : bool Config.T
     1.7 -  val ghc_options : string Config.T
     1.8 +  val ghc_options : string Config.T  (* FIXME prefer settings, i.e. getenv (!?) *)
     1.9    val active : bool Config.T
    1.10    datatype counterexample = Universal_Counterexample of (term * counterexample)
    1.11      | Existential_Counterexample of (term * counterexample) list