# HG changeset patch
# User wenzelm
# Date 1158601147 -7200
# Node ID 4dc799edef89b51b865d3b5393ce040bd71f5723
# Parent  f26c8408a67556084f785f784a281f7687122717
Thm.dest_arg;

diff -r f26c8408a675 -r 4dc799edef89 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Sep 18 19:12:50 2006 +0200
+++ b/src/Pure/drule.ML	Mon Sep 18 19:39:07 2006 +0200
@@ -147,29 +147,29 @@
 
 fun dest_binop ct =
   let val (ct1, ct2) = Thm.dest_comb ct
-  in (#2 (Thm.dest_comb ct1), ct2) end;
+  in (Thm.dest_arg ct1, ct2) end;
 
 fun dest_implies ct =
   (case Thm.term_of ct of
-    (Const ("==>", _) $ _ $ _) => dest_binop ct
+    Const ("==>", _) $ _ $ _ => dest_binop ct
   | _ => raise TERM ("dest_implies", [term_of ct]));
 
 fun dest_equals ct =
   (case Thm.term_of ct of
-    (Const ("==", _) $ _ $ _) => dest_binop ct
-    | _ => raise TERM ("dest_equals", [term_of ct]));
+    Const ("==", _) $ _ $ _ => dest_binop ct
+  | _ => raise TERM ("dest_equals", [term_of ct]));
 
 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
 fun strip_imp_prems ct =
-    let val (cA,cB) = dest_implies ct
-    in  cA :: strip_imp_prems cB  end
-    handle TERM _ => [];
+  let val (cA, cB) = dest_implies ct
+  in cA :: strip_imp_prems cB end
+  handle TERM _ => [];
 
 (* A1==>...An==>B  goes to B, where B is not an implication *)
 fun strip_imp_concl ct =
-    case term_of ct of (Const("==>", _) $ _ $ _) =>
-        strip_imp_concl (#2 (Thm.dest_comb ct))
-  | _ => ct;
+  (case Thm.term_of ct of
+    Const ("==>", _) $ _ $ _ => strip_imp_concl (Thm.dest_arg ct)
+  | _ => ct);
 
 (*The premises of a theorem, as a cterm list*)
 val cprems_of = strip_imp_prems o cprop_of;
@@ -215,7 +215,7 @@
 (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
   of the meta-equality returned by the beta_conversion rule.*)
 fun beta_conv x y =
-    #2 (Thm.dest_comb (cprop_of (Thm.beta_conversion false (Thm.capply x y))));
+  Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.capply x y)));
 
 fun plain_prop_of raw_thm =
   let
@@ -606,7 +606,7 @@
 
 fun extensional eq =
   let val eq' =
-    abstract_rule "x" (snd (Thm.dest_comb (fst (dest_equals (cprop_of eq))))) eq
+    abstract_rule "x" (Thm.dest_arg (fst (dest_equals (cprop_of eq)))) eq
   in equal_elim (eta_conversion (cprop_of eq')) eq' end;
 
 val equals_cong =
@@ -957,7 +957,7 @@
 fun dest_term th =
   let val cprop = Thm.cprop_of th in
     if can Logic.dest_term (Thm.term_of cprop) then
-      #2 (Thm.dest_comb cprop)
+      Thm.dest_arg cprop
     else raise THM ("dest_term", 0, [th])
   end;
 
@@ -995,7 +995,7 @@
       if forall is_none cTs then thm
       else Thm.instantiate
         (map tyinst_of (zip_vars (rev (fold_terms Term.add_tvars thm [])) cTs), []) thm;
-    val thm'' = 
+    val thm'' =
       if forall is_none cts then thm'
       else Thm.instantiate
         ([], map inst_of (zip_vars (rev (fold_terms Term.add_vars thm' [])) cts)) thm';
diff -r f26c8408a675 -r 4dc799edef89 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Sep 18 19:12:50 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Sep 18 19:39:07 2006 +0200
@@ -452,7 +452,7 @@
     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
     val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
-    val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
+    val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
     val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
     val erhs = Envir.eta_contract (term_of rhs);
     val perm =
diff -r f26c8408a675 -r 4dc799edef89 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Mon Sep 18 19:12:50 2006 +0200
+++ b/src/Pure/subgoal.ML	Mon Sep 18 19:39:07 2006 +0200
@@ -47,7 +47,7 @@
       fun export_closed th =
         let
           val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
-          val vs = map (#2 o Thm.dest_comb o Drule.strip_imp_concl o Thm.cprop_of) params';
+          val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
         in Drule.forall_intr_list vs th' end;
       fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
     in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
diff -r f26c8408a675 -r 4dc799edef89 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Sep 18 19:12:50 2006 +0200
+++ b/src/Pure/variable.ML	Mon Sep 18 19:39:07 2006 +0200
@@ -412,8 +412,8 @@
 (* focus on outermost parameters *)
 
 fun forall_elim_prop t prop =
-  Thm.beta_conversion false (Thm.capply (#2 (Thm.dest_comb prop)) t)
-  |> Thm.cprop_of |> Thm.dest_comb |> #2;
+  Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
+  |> Thm.cprop_of |> Thm.dest_arg;
 
 fun focus goal ctxt =
   let