# HG changeset patch
# User wenzelm
# Date 965081947 -7200
# Node ID 708a8a05497dc851e148ab9dde9528c53a50891a
# Parent  9c438a65be0a3406757a16e9d71e063c858bf08a
added has_meta_prems;

diff -r 9c438a65be0a -r 708a8a05497d src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Aug 01 00:18:40 2000 +0200
+++ b/src/Pure/logic.ML	Tue Aug 01 00:19:07 2000 +0200
@@ -29,6 +29,7 @@
   val strip_flexpairs   : term -> (term*term)list * term
   val skip_flexpairs    : term -> term
   val strip_horn        : term -> (term*term)list * term list * term
+  val has_meta_prems    : term -> int -> bool
   val mk_cond_defpair   : term list -> term * term -> string * term
   val mk_defpair        : term * term -> string * term
   val mk_type           : typ -> term
@@ -154,6 +155,19 @@
   let val (tpairs,horn) = strip_flexpairs A
   in  (tpairs, strip_imp_prems horn, strip_imp_concl horn)   end;
 
+(*test for meta connectives in prems of a 'subgoal'*)
+fun has_meta_prems prop i =
+  let
+    fun is_meta (Const ("==>", _) $ _ $ _) = true
+      | is_meta (Const ("all", _) $ _) = true
+      | is_meta _ = false;
+    val horn = skip_flexpairs prop;
+  in
+    (case strip_prems (i, [], horn) of
+      (B :: _, _) => exists is_meta (strip_imp_prems B)
+    | _ => false) handle TERM _ => false
+  end;
+
 
 (** definitions **)
 
@@ -251,6 +265,7 @@
   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   | strip_params B = [];
 
+
 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
     where j is the total number of parameters (precomputed)
   If n>0 then deletes assumption n. *)