src/Tools/Argo/argo_rewr.ML

       let val ((e, c2), c1) = cv e |>> seq cvs
       in (e, Argo_Proof.mk_then_conv c1 c2) end
 
 fun on_args f (Argo_Expr.E (k, es)) =
   let val (es, cs) = split_list (f es)
-  in (Argo_Expr.E (k, es), Argo_Proof.mk_args_conv cs) end
+  in (Argo_Expr.E (k, es), Argo_Proof.mk_args_conv k cs) end
 
 fun args cv e = on_args (map cv) e
 
 fun all_args cv k (e as Argo_Expr.E (k', _)) = if k = k' then args (all_args cv k) e else cv e