src/Pure/logic.ML
changeset 23597 ab67175ca8a5
parent 23418 c195f6f13769
child 24258 2f399483535a
     1.1 --- a/src/Pure/logic.ML	Thu Jul 05 20:01:33 2007 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jul 05 20:01:34 2007 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4    val strip_assums_hyp: term -> term list
     1.5    val strip_assums_concl: term -> term
     1.6    val strip_params: term -> (string * typ) list
     1.7 -  val has_meta_prems: term -> int -> bool
     1.8 +  val has_meta_prems: term -> bool
     1.9    val flatten_params: int -> term -> term
    1.10    val auto_rename: bool ref
    1.11    val set_rename_prefix: string -> unit
    1.12 @@ -448,18 +448,17 @@
    1.13    | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
    1.14    | strip_params B = [];
    1.15  
    1.16 -(*test for meta connectives in prems of a 'subgoal'*)
    1.17 -fun has_meta_prems prop i =
    1.18 +(*test for nested meta connectives in prems*)
    1.19 +val has_meta_prems =
    1.20    let
    1.21 -    fun is_meta (Const ("==>", _) $ _ $ _) = true
    1.22 -      | is_meta (Const ("==", _) $ _ $ _) = true
    1.23 +    fun is_meta (Const ("==", _) $ _ $ _) = true
    1.24 +      | is_meta (Const ("==>", _) $ _ $ _) = true
    1.25        | is_meta (Const ("all", _) $ _) = true
    1.26        | is_meta _ = false;
    1.27 -  in
    1.28 -    (case strip_prems (i, [], prop) of
    1.29 -      (B :: _, _) => exists is_meta (strip_assums_hyp B)
    1.30 -    | _ => false) handle TERM _ => false
    1.31 -  end;
    1.32 +    fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
    1.33 +      | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
    1.34 +      | ex_meta _ = false;
    1.35 +  in ex_meta end;
    1.36  
    1.37  (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
    1.38      where j is the total number of parameters (precomputed)