| changeset 77879 | dd222e2af01a |
| parent 74648 | d1117655110c |
| child 80910 | 406a85a25189 |
--- a/src/HOL/Tools/Argo/argo_tactic.ML Tue Apr 18 21:47:40 2023 +0200 +++ b/src/HOL/Tools/Argo/argo_tactic.ML Tue Apr 18 22:24:48 2023 +0200 @@ -656,7 +656,7 @@ (* normalizing goals *) -fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make [(v, ct)]) +fun instantiate v ct = Thm.instantiate (TVars.empty, Vars.make1 (v, ct)) fun instantiate_elim_rule thm = let