removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Sep 19 16:18:30 2011 +0200
1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Sep 19 16:18:33 2011 +0200
1.3 @@ -380,8 +380,7 @@
1.4 Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property})
1.5 $ Abs (x, T, t)
1.6 in
1.7 - fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $
1.8 - (list_comb (t , map Bound (((length qs) - 1) downto 0))))
1.9 + fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t)
1.10 end
1.11
1.12 fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
1.13 @@ -415,19 +414,13 @@
1.14 apfst (map2 pair qs1) (f (qs2, t)) end
1.15 val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
1.16 val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
1.17 - val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
1.18 - (* FIXME proper naming convention for local_theory *)
1.19 - val ((prop_def, _), ctxt') =
1.20 - Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
1.21 - ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
1.22 - val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
1.23 val (counterexample, result) = dynamic_value_strict (true, opts)
1.24 (Existential_Counterexample.get, Existential_Counterexample.put,
1.25 "Narrowing_Generators.put_existential_counterexample")
1.26 - thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def')
1.27 + thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
1.28 in
1.29 Quickcheck.Result
1.30 - {counterexample = Option.map (mk_terms ctxt' qs) counterexample,
1.31 + {counterexample = Option.map (mk_terms ctxt qs) counterexample,
1.32 evaluation_terms = Option.map (K []) counterexample,
1.33 timings = #timings (dest_result result), reports = #reports (dest_result result)}
1.34 end