1.1 --- a/src/Pure/drule.ML	Mon Sep 18 19:12:50 2006 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Sep 18 19:39:07 2006 +0200
     1.3 @@ -147,29 +147,29 @@
     1.4  
     1.5  fun dest_binop ct =
     1.6    let val (ct1, ct2) = Thm.dest_comb ct
     1.7 -  in (#2 (Thm.dest_comb ct1), ct2) end;
     1.8 +  in (Thm.dest_arg ct1, ct2) end;
     1.9  
    1.10  fun dest_implies ct =
    1.11    (case Thm.term_of ct of
    1.12 -    (Const ("==>", _) $ _ $ _) => dest_binop ct
    1.13 +    Const ("==>", _) $ _ $ _ => dest_binop ct
    1.14    | _ => raise TERM ("dest_implies", [term_of ct]));
    1.15  
    1.16  fun dest_equals ct =
    1.17    (case Thm.term_of ct of
    1.18 -    (Const ("==", _) $ _ $ _) => dest_binop ct
    1.19 -    | _ => raise TERM ("dest_equals", [term_of ct]));
    1.20 +    Const ("==", _) $ _ $ _ => dest_binop ct
    1.21 +  | _ => raise TERM ("dest_equals", [term_of ct]));
    1.22  
    1.23  (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    1.24  fun strip_imp_prems ct =
    1.25 -    let val (cA,cB) = dest_implies ct
    1.26 -    in  cA :: strip_imp_prems cB  end
    1.27 -    handle TERM _ => [];
    1.28 +  let val (cA, cB) = dest_implies ct
    1.29 +  in cA :: strip_imp_prems cB end
    1.30 +  handle TERM _ => [];
    1.31  
    1.32  (* A1==>...An==>B  goes to B, where B is not an implication *)
    1.33  fun strip_imp_concl ct =
    1.34 -    case term_of ct of (Const("==>", _) $ _ $ _) =>
    1.35 -        strip_imp_concl (#2 (Thm.dest_comb ct))
    1.36 -  | _ => ct;
    1.37 +  (case Thm.term_of ct of
    1.38 +    Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
    1.39 +  | _ => ct);
    1.40  
    1.41  (*The premises of a theorem, as a cterm list*)
    1.42  val cprems_of = strip_imp_prems o cprop_of;
    1.43 @@ -215,7 +215,7 @@
    1.44  (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
    1.45    of the meta-equality returned by the beta_conversion rule.*)
    1.46  fun beta_conv x y =
    1.47 -    #2 (Thm.dest_comb (cprop_of (Thm.beta_conversion false (Thm.capply x y))));
    1.48 +  Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.capply x y)));
    1.49  
    1.50  fun plain_prop_of raw_thm =
    1.51    let
    1.52 @@ -606,7 +606,7 @@
    1.53  
    1.54  fun extensional eq =
    1.55    let val eq' =
    1.56 -    abstract_rule "x" (snd (Thm.dest_comb (fst (dest_equals (cprop_of eq))))) eq
    1.57 +    abstract_rule "x" (Thm.dest_arg (fst (dest_equals (cprop_of eq)))) eq
    1.58    in equal_elim (eta_conversion (cprop_of eq')) eq' end;
    1.59  
    1.60  val equals_cong =
    1.61 @@ -957,7 +957,7 @@
    1.62  fun dest_term th =
    1.63    let val cprop = Thm.cprop_of th in
    1.64      if can Logic.dest_term (Thm.term_of cprop) then
    1.65 -      #2 (Thm.dest_comb cprop)
    1.66 +      Thm.dest_arg cprop
    1.67      else raise THM ("dest_term", 0, [th])
    1.68    end;
    1.69  
    1.70 @@ -995,7 +995,7 @@
    1.71        if forall is_none cTs then thm
    1.72        else Thm.instantiate
    1.73          (map tyinst_of (zip_vars (rev (fold_terms Term.add_tvars thm [])) cTs), []) thm;
    1.74 -    val thm'' = 
    1.75 +    val thm'' =
    1.76        if forall is_none cts then thm'
    1.77        else Thm.instantiate
    1.78          ([], map inst_of (zip_vars (rev (fold_terms Term.add_vars thm' [])) cts)) thm';

     2.1 --- a/src/Pure/meta_simplifier.ML	Mon Sep 18 19:12:50 2006 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Mon Sep 18 19:39:07 2006 +0200
     2.3 @@ -452,7 +452,7 @@
     2.4      val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
     2.5      val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
     2.6        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     2.7 -    val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
     2.8 +    val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
     2.9      val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
    2.10      val erhs = Envir.eta_contract (term_of rhs);
    2.11      val perm =

     3.1 --- a/src/Pure/subgoal.ML	Mon Sep 18 19:12:50 2006 +0200
     3.2 +++ b/src/Pure/subgoal.ML	Mon Sep 18 19:39:07 2006 +0200
     3.3 @@ -47,7 +47,7 @@
     3.4        fun export_closed th =
     3.5          let
     3.6            val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
     3.7 -          val vs = map (#2 o Thm.dest_comb o Drule.strip_imp_concl o Thm.cprop_of) params';
     3.8 +          val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
     3.9          in Drule.forall_intr_list vs th' end;
    3.10        fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
    3.11      in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end

     4.1 --- a/src/Pure/variable.ML	Mon Sep 18 19:12:50 2006 +0200
     4.2 +++ b/src/Pure/variable.ML	Mon Sep 18 19:39:07 2006 +0200
     4.3 @@ -412,8 +412,8 @@
     4.4  (* focus on outermost parameters *)
     4.5  
     4.6  fun forall_elim_prop t prop =
     4.7 -  Thm.beta_conversion false (Thm.capply (#2 (Thm.dest_comb prop)) t)
     4.8 -  |> Thm.cprop_of |> Thm.dest_comb |> #2;
     4.9 +  Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
    4.10 +  |> Thm.cprop_of |> Thm.dest_arg;
    4.11  
    4.12  fun focus goal ctxt =
    4.13    let