src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43619 3803869014aa
parent 43602 8c89a1fb30f2
child 43702 24fb44c1086a
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 01 15:14:44 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 01 15:16:03 2011 +0200
     1.3 @@ -408,8 +408,10 @@
     1.4          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
     1.5          val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
     1.6          val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
     1.7 -        val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
     1.8 -          ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
     1.9 +        (* FIXME proper naming convention for local_theory *)
    1.10 +        val ((prop_def, _), ctxt') =
    1.11 +          Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
    1.12 +            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
    1.13          val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
    1.14          val (counterexample, result) = dynamic_value_strict (true, opts)
    1.15            (Existential_Counterexample.get, Existential_Counterexample.put,