changeset 74503 | 403ce50e6a2a |
parent 74375 | ba880f3a4e52 |
child 74506 | d97c48dc87fa |
--- a/src/HOL/Hoare/hoare_tac.ML Mon Oct 11 21:55:21 2021 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Tue Oct 12 20:57:43 2021 +0200 @@ -71,7 +71,7 @@ fun get_vars c = let val d = Logic.strip_assums_concl c; - val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d; + val Const _ $ pre $ _ $ _ $ _ = HOLogic.dest_Trueprop d; in mk_vars pre end; fun mk_CollectC tm =