src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 45002 df36896aae0f
parent 44926 de3ed037c9a5
child 45039 632a033616e9
     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