--- a/src/HOL/Hoare/hoare_tac.ML Wed Oct 13 00:02:35 2021 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Wed Oct 13 00:07:06 2021 +0200
@@ -71,7 +71,10 @@
fun get_vars c =
let
val d = Logic.strip_assums_concl c;
- val Const _ $ pre $ _ $ _ $ _ = HOLogic.dest_Trueprop d;
+ val pre =
+ case HOLogic.dest_Trueprop d of
+ Const _ $ pre $ _ $ _ $ _ => pre
+ | Const _ $ pre $ _ $ _ => pre \<comment> \<open>support for \<^file>\<open>~~/src/HOL/Isar_Examples/Hoare.thy\<close>\<close>
in mk_vars pre end;
fun mk_CollectC tm =