src/Pure/drule.ML
changeset 708 8422e50adce0
parent 668 0d0923eb0f0d
child 776 df8f91c0e57c
--- 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