1.1 --- a/src/Pure/logic.ML	Mon Aug 21 17:54:43 2000 +0200
     1.2 +++ b/src/Pure/logic.ML	Mon Aug 21 18:16:47 2000 +0200
     1.3 @@ -29,7 +29,6 @@
     1.4    val strip_flexpairs   : term -> (term*term)list * term
     1.5    val skip_flexpairs    : term -> term
     1.6    val strip_horn        : term -> (term*term)list * term list * term
     1.7 -  val has_meta_prems    : term -> int -> bool
     1.8    val mk_cond_defpair   : term list -> term * term -> string * term
     1.9    val mk_defpair        : term * term -> string * term
    1.10    val mk_type           : typ -> term
    1.11 @@ -46,6 +45,7 @@
    1.12    val strip_assums_hyp  : term -> term list
    1.13    val strip_assums_concl: term -> term
    1.14    val strip_params      : term -> (string * typ) list
    1.15 +  val has_meta_prems    : term -> int -> bool
    1.16    val flatten_params    : int -> term -> term
    1.17    val auto_rename       : bool ref
    1.18    val set_rename_prefix : string -> unit
    1.19 @@ -155,19 +155,6 @@
    1.20    let val (tpairs,horn) = strip_flexpairs A
    1.21    in  (tpairs, strip_imp_prems horn, strip_imp_concl horn)   end;
    1.22  
    1.23 -(*test for meta connectives in prems of a 'subgoal'*)
    1.24 -fun has_meta_prems prop i =
    1.25 -  let
    1.26 -    fun is_meta (Const ("==>", _) $ _ $ _) = true
    1.27 -      | is_meta (Const ("all", _) $ _) = true
    1.28 -      | is_meta _ = false;
    1.29 -    val horn = skip_flexpairs prop;
    1.30 -  in
    1.31 -    (case strip_prems (i, [], horn) of
    1.32 -      (B :: _, _) => exists is_meta (strip_imp_prems B)
    1.33 -    | _ => false) handle TERM _ => false
    1.34 -  end;
    1.35 -
    1.36  
    1.37  (** definitions **)
    1.38  
    1.39 @@ -265,6 +252,18 @@
    1.40    | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
    1.41    | strip_params B = [];
    1.42  
    1.43 +(*test for meta connectives in prems of a 'subgoal'*)
    1.44 +fun has_meta_prems prop i =
    1.45 +  let
    1.46 +    fun is_meta (Const ("==>", _) $ _ $ _) = true
    1.47 +      | is_meta (Const ("all", _) $ _) = true
    1.48 +      | is_meta _ = false;
    1.49 +    val horn = skip_flexpairs prop;
    1.50 +  in
    1.51 +    (case strip_prems (i, [], horn) of
    1.52 +      (B :: _, _) => exists is_meta (strip_assums_hyp B)
    1.53 +    | _ => false) handle TERM _ => false
    1.54 +  end;
    1.55  
    1.56  (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
    1.57      where j is the total number of parameters (precomputed)