# HG changeset patch
# User wenzelm
# Date 1634076426 -7200
# Node ID d97c48dc87fa4cf898b9427abe6a94eeec0ebc5d
# Parent  ce8152fb021bbef27ea248852f131430dffbe48f
support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);

diff -r ce8152fb021b -r d97c48dc87fa src/HOL/Hoare/hoare_tac.ML
--- 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 =