src/HOL/Tools/Argo/argo_tactic.ML
changeset 66301 8a6a89d6cf2b
parent 63992 3aa9837d05c7
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Tools/Argo/argo_tactic.ML	Mon Jul 31 15:38:21 2017 +0100
     1.2 +++ b/src/HOL/Tools/Argo/argo_tactic.ML	Tue Aug 01 07:26:23 2017 +0200
     1.3 @@ -474,7 +474,9 @@
     1.4  fun replay_conv _ Argo_Proof.Keep_Conv ct = Conv.all_conv ct
     1.5    | replay_conv ctxt (Argo_Proof.Then_Conv (c1, c2)) ct = 
     1.6        (replay_conv ctxt c1 then_conv replay_conv ctxt c2) ct
     1.7 -  | replay_conv ctxt (Argo_Proof.Args_Conv cs) ct = replay_args_conv ctxt cs ct
     1.8 +  | replay_conv ctxt (Argo_Proof.Args_Conv (Argo_Expr.App, [c1, c2])) ct =
     1.9 +      Conv.combination_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
    1.10 +  | replay_conv ctxt (Argo_Proof.Args_Conv (_, cs)) ct = replay_args_conv ctxt cs ct
    1.11    | replay_conv ctxt (Argo_Proof.Rewr_Conv r) ct = replay_rewr ctxt r ct
    1.12  
    1.13  and replay_args_conv _ [] ct = Conv.all_conv ct