# HG changeset patch
# User paulson
# Date 843493543 -7200
# Node ID 3411fe560611e937643307c36af6319c07b39316
# Parent  b48f066d52dc88d12a314160309d142ed737a081
New operations on cterms.  Now same names as in Logic

diff -r b48f066d52dc -r 3411fe560611 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Sep 23 17:42:56 1996 +0200
+++ b/src/Pure/drule.ML	Mon Sep 23 17:45:43 1996 +0200
@@ -17,8 +17,6 @@
   val COMP		: thm * thm -> thm
   val compose		: thm * int * thm -> thm list
   val cprems_of		: thm -> cterm list
-  val cskip_flexpairs	: cterm -> cterm
-  val cstrip_imp_prems	: cterm -> cterm list
   val cterm_instantiate	: (cterm*cterm)list -> thm -> thm
   val cut_rl		: thm
   val equal_abs_elim	: cterm  -> thm -> thm
@@ -35,7 +33,7 @@
   val forall_elim_vars	: int -> thm -> thm
   val implies_elim_list	: thm -> thm list -> thm
   val implies_intr_list	: cterm list -> thm -> thm
-  val dest_cimplies     : cterm -> cterm * cterm
+  val dest_implies      : cterm -> cterm * cterm
   val MRL		: thm list list * thm list -> thm list
   val MRS		: thm list * thm -> thm
   val read_instantiate	: (string*string)list -> thm -> thm
@@ -46,6 +44,7 @@
                   -> string list -> (string*string)list
                   -> (indexname*ctyp)list * (cterm*cterm)list
   val reflexive_thm	: thm
+  val refl_implies      : thm
   val revcut_rl		: thm
   val rewrite_goal_rule	: bool*bool -> (meta_simpset -> thm -> thm option)
         -> meta_simpset -> int -> thm -> thm
@@ -56,7 +55,9 @@
   val RL		: thm list * thm list -> thm list
   val RLN		: thm list * (int * thm list) -> thm list
   val size_of_thm	: thm -> int
+  val skip_flexpairs	: cterm -> cterm
   val standard		: thm -> thm
+  val strip_imp_prems	: cterm -> cterm list
   val swap_prems_rl     : thm
   val symmetric_thm	: thm
   val thin_rl		: thm
@@ -194,32 +195,38 @@
 
 (** some cterm->cterm operations: much faster than calling cterm_of! **)
 
+(** SAME NAMES as in structure Logic: use compound identifiers! **)
+
 (*dest_implies for cterms. Note T=prop below*)
-fun dest_cimplies ct =
-  (let val (ct1, ct2) = dest_comb ct
-       val {t, ...} = rep_cterm ct1;
-   in case head_of t of
-          Const("==>", _) => (snd (dest_comb ct1), ct2)
-        | _ => raise TERM ("dest_cimplies", [term_of ct])
-   end
-  ) handle CTERM "dest_comb" => raise TERM ("dest_cimplies", [term_of ct]);
+fun dest_implies ct =
+    case term_of ct of 
+	(Const("==>", _) $ _ $ _) => 
+	    let val (ct1,ct2) = dest_comb ct
+	    in  (#2 (dest_comb ct1), ct2)  end	     
+      | _ => raise TERM ("dest_implies", [term_of ct]) ;
 
 
 (*Discard flexflex pairs; return a cterm*)
-fun cskip_flexpairs ct =
+fun skip_flexpairs ct =
     case term_of ct of
 	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
-	    cskip_flexpairs (#2 (dest_cimplies ct))
+	    skip_flexpairs (#2 (dest_implies ct))
       | _ => ct;
 
 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
-fun cstrip_imp_prems ct =
-    let val (cA,cB) = dest_cimplies ct
-    in  cA :: cstrip_imp_prems cB  end
+fun strip_imp_prems ct =
+    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 (dest_comb ct))
+  | _ => ct;
+
 (*The premises of a theorem, as a cterm list*)
-val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of;
+val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of;
 
 
 (** reading of instantiations **)
@@ -518,17 +525,17 @@
 
 (** Below, a "conversion" has type cterm -> thm **)
 
-val refl_cimplies = reflexive (cterm_of Sign.proto_pure implies);
+val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
 
 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
 (*Do not rewrite flex-flex pairs*)
 fun goals_conv pred cv =
   let fun gconv i ct =
-        let val (A,B) = dest_cimplies ct
+        let val (A,B) = dest_implies ct
             val (thA,j) = case term_of A of
                   Const("=?=",_)$_$_ => (reflexive A, i)
                 | _ => (if pred i then cv A else reflexive A, i+1)
-        in  combination (combination refl_cimplies thA) (gconv j B) end
+        in  combination (combination refl_implies thA) (gconv j B) end
         handle TERM _ => reflexive ct
   in gconv 1 end;
 
@@ -576,7 +583,6 @@
 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th);
 
 local
-  open Logic
   val alpha = TVar(("'a",0), [])     (*  type ?'a::{}  *)
   fun err th = raise THM("flexpair_inst: ", 0, [th])
   fun flexpair_inst def th =