-let rec mk_atomic st dtext what =
- if T.is_atomic what then
- match what with
- | C.ARel (_, _, _, name) -> convert st ~name what, what
- | _ -> [], what
- else
- let name = defined_premise in
- let script = convert st ~name what in
- script @ mk_fwd_proof st dtext name what, T.mk_arel 0 name
+let rec mk_arg st = function
+ | C.ARel (_, _, _, name) as what -> convert st ~name what, what
+ | what -> [], what