# HG changeset patch
# User lcp
# Date 784806410 -3600
# Node ID 8422e50adce0519d3eb28aec842fd6c5d2bb0359
# Parent  04d661f1d2f89e1fecb1c0b5337fd526dfbc1f9c
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations

diff -r 04d661f1d2f8 -r 8422e50adce0 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Nov 14 10:41:25 1994 +0100
+++ b/src/Pure/drule.ML	Mon Nov 14 10:46:50 1994 +0100
@@ -18,6 +18,9 @@
   val assume_ax		: theory -> string -> thm
   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
@@ -217,6 +220,25 @@
 
 (**** More derived rules and operations on theorems ****)
 
+(** some cterm->cterm operations: much faster than calling cterm_of! **)
+
+(*Discard flexflex pairs; return a cterm*)
+fun cskip_flexpairs ct =
+    case term_of ct of
+	(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) =>
+	    cskip_flexpairs (#2 (dest_cimplies 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
+    handle TERM _ => [];
+
+(*The premises of a theorem, as a cterm list*)
+val cprems_of = cstrip_imp_prems o cskip_flexpairs o cprop_of;
+
+
 (** reading of instantiations **)
 
 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v