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