1418 cond_timeit (Config.get ctxt Quickcheck.timing) "Proving equations...." (fn _ => |
1418 cond_timeit (Config.get ctxt Quickcheck.timing) "Proving equations...." (fn _ => |
1419 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
1419 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
1420 val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds |
1420 val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds |
1421 (maps_modes result_thms) |
1421 (maps_modes result_thms) |
1422 val qname = #qname (dest_steps steps) |
1422 val qname = #qname (dest_steps steps) |
1423 (* FIXME !? *) |
1423 val attrib = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I) |
1424 val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute |
|
1425 (fn thm => Context.mapping (Code.add_eqn thm) I)))) |
|
1426 val thy''' = |
1424 val thy''' = |
1427 cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ => |
1425 cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ => |
1428 fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss |
1426 fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss |
1429 [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), |
1427 [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), |
1430 [attrib thy ])] thy)) |
1428 [attrib])] thy)) |
1431 result_thms' thy'' |> Theory.checkpoint) |
1429 result_thms' thy'' |> Theory.checkpoint) |
1432 in |
1430 in |
1433 thy''' |
1431 thy''' |
1434 end |
1432 end |
1435 |
1433 |