Lines Matching defs:arg
2980 let val arg = (combine_qps (bqp::args)) in
2981 HEURISTIC_QUANT_INSTANTIATE_CONV re min_occs (qp_to_heuristic arg cache_ref_opt) expand_eq (#final_rewrite_thms arg) ctx
2985 val hL = QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE arg
2991 (QUANT_INSTANTIATE_HEURISTIC___PURE_COMBINE arg NONE) v t
3062 let val arg = (combine_qps (bqp::args)) in
3064 arg cache_ref_opt) (#final_rewrite_thms arg) end;
3067 let val arg = (combine_qps (bqp::args)) in
3069 (qp_to_heuristic arg cache_ref_opt)
3070 (#final_rewrite_thms arg) []) end;