--- 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