183 val time = Time.toMilliseconds (#cpu (end_timing start)) |
183 val time = Time.toMilliseconds (#cpu (end_timing start)) |
184 in (Exn.release result, (description, time)) end |
184 in (Exn.release result, (description, time)) end |
185 |
185 |
186 fun compile_term compilation options ctxt t = |
186 fun compile_term compilation options ctxt t = |
187 let |
187 let |
188 val ctxt' = ProofContext.theory (Context.copy_thy) ctxt |
188 val thy = Theory.copy (ProofContext.theory_of ctxt) |
189 val thy = (ProofContext.theory_of ctxt') |
|
190 val (vs, t') = strip_abs t |
189 val (vs, t') = strip_abs t |
191 val vs' = Variable.variant_frees ctxt' [] vs |
190 val vs' = Variable.variant_frees ctxt [] vs |
192 val t'' = subst_bounds (map Free (rev vs'), t') |
191 val t'' = subst_bounds (map Free (rev vs'), t') |
193 val (prems, concl) = strip_horn t'' |
192 val (prems, concl) = strip_horn t'' |
194 val constname = "pred_compile_quickcheck" |
193 val constname = "pred_compile_quickcheck" |
195 val full_constname = Sign.full_bname thy constname |
194 val full_constname = Sign.full_bname thy constname |
196 val constT = map snd vs' ---> @{typ bool} |
195 val constT = map snd vs' ---> @{typ bool} |