--- 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;
--- a/src/HOL/Hoare/hoareAbort.ML Fri Oct 28 22:27:44 2005 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML Fri Oct 28 22:27:46 2005 +0200
@@ -54,11 +54,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;
--- a/src/HOL/Tools/datatype_aux.ML Fri Oct 28 22:27:44 2005 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Fri Oct 28 22:27:46 2005 +0200
@@ -111,7 +111,7 @@
(List.nth (prems_of st, i - 1)) of
_ $ (_ $ (f $ x) $ (g $ y)) =>
let
- val cong' = lift_rule (st, i) cong;
+ val cong' = Thm.lift_rule (Thm.cgoal_of st i) cong;
val _ $ (_ $ (f' $ x') $ (g' $ y')) =
Logic.strip_assums_concl (prop_of cong');
val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
@@ -151,7 +151,7 @@
val prem = List.nth (prems_of state, i - 1);
val params = Logic.strip_params prem;
val (_, Type (tname, _)) = hd (rev params);
- val exhaustion = lift_rule (state, i) (exh_thm_of tname);
+ val exhaustion = Thm.lift_rule (Thm.cgoal_of state i) (exh_thm_of tname);
val prem' = hd (prems_of exhaustion);
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),