# HG changeset patch
# User wenzelm
# Date 1160353196 -7200
# Node ID 363a9cba29537a5311de51e927f0a7265cf46607
# Parent  905effde63d90a4a357f4772bb5653129c8dd9b4
added dest_equals_lhs;
replaced clhs/crhs_of by lhs/rhs_of;
local_standard: flexflex_unique;
removed strip_shyps_warning;

diff -r 905effde63d9 -r 363a9cba2953 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Oct 09 02:19:55 2006 +0200
+++ b/src/Pure/drule.ML	Mon Oct 09 02:19:56 2006 +0200
@@ -14,6 +14,7 @@
   val list_implies: cterm list * cterm -> cterm
   val dest_implies: cterm -> cterm * cterm
   val dest_equals: cterm -> cterm * cterm
+  val dest_equals_lhs: cterm -> cterm
   val dest_equals_rhs: cterm -> cterm
   val strip_imp_prems: cterm -> cterm list
   val strip_imp_concl: cterm -> cterm
@@ -24,7 +25,6 @@
     (indexname -> typ option) * (indexname -> sort option) -> string list ->
     (indexname * string) list -> (ctyp * ctyp) list * (cterm * cterm) list
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
-  val strip_shyps_warning: thm -> thm
   val forall_intr_list: cterm list -> thm -> thm
   val forall_intr_frees: thm -> thm
   val forall_intr_vars: thm -> thm
@@ -89,8 +89,8 @@
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
   val strip_type: ctyp -> ctyp list * ctyp
-  val clhs_of: thm -> cterm
-  val crhs_of: thm -> cterm
+  val lhs_of: thm -> cterm
+  val rhs_of: thm -> cterm
   val beta_conv: cterm -> cterm -> cterm
   val plain_prop_of: thm -> term
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
@@ -159,11 +159,19 @@
     Const ("==", _) $ _ $ _ => Thm.dest_binop ct
   | _ => raise TERM ("dest_equals", [Thm.term_of ct]));
 
+fun dest_equals_lhs ct =
+  (case Thm.term_of ct of
+    Const ("==", _) $ _ $ _ => #1 (Thm.dest_binop ct)
+  | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
+
 fun dest_equals_rhs ct =
   (case Thm.term_of ct of
     Const ("==", _) $ _ $ _ => Thm.dest_arg ct
   | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
 
+val lhs_of = dest_equals_lhs o Thm.cprop_of;
+val rhs_of = dest_equals_rhs o Thm.cprop_of;
+
 (* 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
@@ -217,18 +225,6 @@
       in (cT1 :: cTs, cT') end
   | _ => ([], cT));
 
-fun clhs_of th =
-  case strip_comb (cprop_of th) of
-      (f, [x, _]) =>
-          (case term_of f of Const ("==", _) => x | _ => raise THM ("clhs_of", 0, [th]))
-    | _ => raise THM ("clhs_of", 1, [th]);
-
-fun crhs_of th =
-  case strip_comb (cprop_of th) of
-      (f, [_, x]) =>
-          (case term_of f of Const ("==", _) => x | _ => raise THM ("crhs_of", 0, [th]))
-    | _ => raise THM ("crhs_of", 1, [th]);
-
 (*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 =
@@ -336,17 +332,6 @@
   fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
     (fold_terms Term.add_tvars th []) th;
 
-fun strip_shyps_warning thm =
-  let
-    val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.theory_of_thm thm);
-    val thm' = Thm.strip_shyps thm;
-    val xshyps = Thm.extra_shyps thm';
-  in
-    if null xshyps then ()
-    else warning ("Pending sort hypotheses: " ^ commas (map str_of_sort xshyps));
-    thm'
-  end;
-
 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev forall_intr;
 
@@ -445,7 +430,7 @@
   #> `Thm.maxidx_of
   #-> (fn maxidx =>
     forall_elim_vars (maxidx + 1)
-    #> strip_shyps_warning
+    #> Thm.strip_shyps
     #> zero_var_indexes
     #> Thm.varifyT
     #> Thm.compress);
@@ -456,7 +441,8 @@
   #> close_derivation;
 
 val local_standard =
-  strip_shyps
+  flexflex_unique
+  #> Thm.strip_shyps
   #> zero_var_indexes
   #> Thm.compress
   #> close_derivation;