Logic.unprotect;
authorwenzelm
Fri Oct 28 22:27:46 2005 +0200 (2005-10-28)
changeset 18022c1bb6480534f
parent 18021 99d170aebb6e
child 18023 3900037edf3d
Logic.unprotect;
src/HOL/Hoare/hoare.ML
src/HOL/Hoare/hoareAbort.ML
src/HOL/Tools/datatype_aux.ML
     1.1 --- a/src/HOL/Hoare/hoare.ML	Fri Oct 28 22:27:44 2005 +0200
     1.2 +++ b/src/HOL/Hoare/hoare.ML	Fri Oct 28 22:27:46 2005 +0200
     1.3 @@ -53,11 +53,9 @@
     1.4                                              ("fun", [_, T])])) $ _ $ _ => T;
     1.5                   in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
     1.6  
     1.7 -fun dest_Goal (Const ("Goal", _) $ P) = P;
     1.8 -
     1.9  (** maps a goal of the form:
    1.10          1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    1.11 -fun get_vars thm = let  val c = dest_Goal (concl_of (thm));
    1.12 +fun get_vars thm = let  val c = Logic.unprotect (concl_of (thm));
    1.13                          val d = Logic.strip_assums_concl c;
    1.14                          val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    1.15        in mk_vars pre end;
     2.1 --- a/src/HOL/Hoare/hoareAbort.ML	Fri Oct 28 22:27:44 2005 +0200
     2.2 +++ b/src/HOL/Hoare/hoareAbort.ML	Fri Oct 28 22:27:46 2005 +0200
     2.3 @@ -54,11 +54,9 @@
     2.4                                              ("fun", [_, T])])) $ _ $ _ => T;
     2.5                   in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
     2.6  
     2.7 -fun dest_Goal (Const ("Goal", _) $ P) = P;
     2.8 -
     2.9  (** maps a goal of the form:
    2.10          1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
    2.11 -fun get_vars thm = let  val c = dest_Goal (concl_of (thm));
    2.12 +fun get_vars thm = let  val c = Logic.unprotect (concl_of (thm));
    2.13                          val d = Logic.strip_assums_concl c;
    2.14                          val Const _ $ pre $ _ $ _ = dest_Trueprop d;
    2.15        in mk_vars pre end;
     3.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Oct 28 22:27:44 2005 +0200
     3.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Oct 28 22:27:46 2005 +0200
     3.3 @@ -111,7 +111,7 @@
     3.4    (List.nth (prems_of st, i - 1)) of
     3.5      _ $ (_ $ (f $ x) $ (g $ y)) =>
     3.6        let
     3.7 -        val cong' = lift_rule (st, i) cong;
     3.8 +        val cong' = Thm.lift_rule (Thm.cgoal_of st i) cong;
     3.9          val _ $ (_ $ (f' $ x') $ (g' $ y')) =
    3.10            Logic.strip_assums_concl (prop_of cong');
    3.11          val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
    3.12 @@ -151,7 +151,7 @@
    3.13      val prem = List.nth (prems_of state, i - 1);
    3.14      val params = Logic.strip_params prem;
    3.15      val (_, Type (tname, _)) = hd (rev params);
    3.16 -    val exhaustion = lift_rule (state, i) (exh_thm_of tname);
    3.17 +    val exhaustion = Thm.lift_rule (Thm.cgoal_of state i) (exh_thm_of tname);
    3.18      val prem' = hd (prems_of exhaustion);
    3.19      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    3.20      val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),