# HG changeset patch
# User bulwahn
# Date 1316441913 -7200
# Node ID df36896aae0f04676925d26910f5fc9194a0ee66
# Parent  5c8d7d6db682073e422f77b9b766e958d7110723
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

diff -r 5c8d7d6db682 -r df36896aae0f src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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