1419 cond_timeit (Config.get ctxt Quickcheck.timing) "Proving equations...." (fn _ => |
1419 cond_timeit (Config.get ctxt Quickcheck.timing) "Proving equations...." (fn _ => |
1420 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
1420 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
1421 val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds |
1421 val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds |
1422 (maps_modes result_thms) |
1422 (maps_modes result_thms) |
1423 val qname = #qname (dest_steps steps) |
1423 val qname = #qname (dest_steps steps) |
1424 val attrib = Thm.declaration_attribute (fn thm => Context.mapping |
1424 val thy''' = cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." |
1425 (Code.add_eqn (Code.Equation, false) thm) I) |
1425 (fn _ => |
1426 (*FIXME default code equation!?*) |
1426 thy'' |
1427 val thy''' = |
1427 |> fold_map (fn (name, result_thms) => (Global_Theory.add_thmss |
1428 cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ => |
1428 [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [])])) |
1429 fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss |
1429 result_thms' |
1430 [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), |
1430 |-> (fn notes => Code.declare_default_eqns_global (map (rpair true) (flat (flat (notes)))))) |
1431 [attrib])] thy)) |
|
1432 result_thms' thy'') |
|
1433 in |
1431 in |
1434 thy''' |
1432 thy''' |
1435 end |
1433 end |
1436 |
1434 |
1437 fun gen_add_equations steps options names thy = |
1435 fun gen_add_equations steps options names thy = |