--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Sep 19 16:18:30 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Sep 19 16:18:33 2011 +0200
@@ -380,8 +380,7 @@
Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property})
$ Abs (x, T, t)
in
- fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $
- (list_comb (t , map Bound (((length qs) - 1) downto 0))))
+ fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t)
end
fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
@@ -415,19 +414,13 @@
apfst (map2 pair qs1) (f (qs2, t)) end
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
- val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
- (* FIXME proper naming convention for local_theory *)
- val ((prop_def, _), ctxt') =
- Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
- ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
- val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
val (counterexample, result) = dynamic_value_strict (true, opts)
(Existential_Counterexample.get, Existential_Counterexample.put,
"Narrowing_Generators.put_existential_counterexample")
- thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def')
+ thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
in
Quickcheck.Result
- {counterexample = Option.map (mk_terms ctxt' qs) counterexample,
+ {counterexample = Option.map (mk_terms ctxt qs) counterexample,
evaluation_terms = Option.map (K []) counterexample,
timings = #timings (dest_result result), reports = #reports (dest_result result)}
end