--- a/src/HOL/Hoare/hoare.ML Fri Oct 28 22:27:44 2005 +0200
+++ b/src/HOL/Hoare/hoare.ML Fri Oct 28 22:27:46 2005 +0200
@@ -53,11 +53,9 @@
("fun", [_, T])])) $ _ $ _ => T;
in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
-fun dest_Goal (Const ("Goal", _) $ P) = P;
-
(** maps a goal of the form:
1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
-fun get_vars thm = let val c = dest_Goal (concl_of (thm));
+fun get_vars thm = let val c = Logic.unprotect (concl_of (thm));
val d = Logic.strip_assums_concl c;
val Const _ $ pre $ _ $ _ = dest_Trueprop d;
in mk_vars pre end;