# HG changeset patch
# User wenzelm
# Date 966874607 -7200
# Node ID 48cefe2daf32878cc028edec18bc7db0974330d0
# Parent  3572fc1dbe6ba0ffe99ffc3e076f4a5b6a6242c0
fixed has_meta_prems: strip_assums_hyp;

diff -r 3572fc1dbe6b -r 48cefe2daf32 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Aug 21 17:54:43 2000 +0200
+++ b/src/Pure/logic.ML	Mon Aug 21 18:16:47 2000 +0200
@@ -29,7 +29,6 @@
   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
@@ -46,6 +45,7 @@
   val strip_assums_hyp  : term -> term list
   val strip_assums_concl: term -> term
   val strip_params      : term -> (string * typ) list
+  val has_meta_prems    : term -> int -> bool
   val flatten_params    : int -> term -> term
   val auto_rename       : bool ref
   val set_rename_prefix : string -> unit
@@ -155,19 +155,6 @@
   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 **)
 
@@ -265,6 +252,18 @@
   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   | strip_params B = [];
 
+(*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_assums_hyp B)
+    | _ => false) handle TERM _ => false
+  end;
 
 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
     where j is the total number of parameters (precomputed)