equal
deleted
inserted
replaced
1015 |
1015 |
1016 val active = Attrib.setup_config_bool @{binding quickcheck_prolog_active} (K true); |
1016 val active = Attrib.setup_config_bool @{binding quickcheck_prolog_active} (K true); |
1017 |
1017 |
1018 fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) = |
1018 fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) = |
1019 let |
1019 let |
1020 val t' = list_abs_free (Term.add_frees t [], t) |
1020 val t' = fold_rev absfree (Term.add_frees t []) t |
1021 val options = code_options_of (Proof_Context.theory_of ctxt) |
1021 val options = code_options_of (Proof_Context.theory_of ctxt) |
1022 val thy = Theory.copy (Proof_Context.theory_of ctxt) |
1022 val thy = Theory.copy (Proof_Context.theory_of ctxt) |
1023 val ((((full_constname, constT), vs'), intro), thy1) = |
1023 val ((((full_constname, constT), vs'), intro), thy1) = |
1024 Predicate_Compile_Aux.define_quickcheck_predicate t' thy |
1024 Predicate_Compile_Aux.define_quickcheck_predicate t' thy |
1025 val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 |
1025 val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 |