1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Apr 19 13:11:35 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Apr 20 04:20:06 2006 +0200
     1.3 @@ -224,29 +224,31 @@
     1.4    | upgrade_lg FOL lg = lg; 
     1.5  
     1.6  (* check types *)
     1.7 -fun has_bool (Type("bool",_)) = true
     1.8 -  | has_bool (Type(_, Ts)) = exists has_bool Ts
     1.9 -  | has_bool _ = false;
    1.10 +fun has_bool_hfn (Type("bool",_)) = true
    1.11 +  | has_bool_hfn (Type("fun",_)) = true
    1.12 +  | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
    1.13 +  | has_bool_hfn _ = false;
    1.14  
    1.15 -fun has_bool_arg tp = 
    1.16 +fun is_hol_fn tp =
    1.17      let val (targs,tr) = strip_type tp
    1.18      in
    1.19 -	exists has_bool targs
    1.20 +	exists (has_bool_hfn) (tr::targs)
    1.21      end;
    1.22  
    1.23 -fun is_fn_tp (Type("fun",_)) = true
    1.24 -  | is_fn_tp _ = false;
    1.25 -
    1.26 +fun is_hol_pred tp =
    1.27 +    let val (targs,tr) = strip_type tp
    1.28 +    in
    1.29 +	exists (has_bool_hfn) targs
    1.30 +    end;
    1.31  
    1.32  exception FN_LG of term;
    1.33  
    1.34  fun fn_lg (t as Const(f,tp)) (lg,seen) = 
    1.35 -    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
    1.36 +    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
    1.37    | fn_lg (t as Free(f,tp)) (lg,seen) = 
    1.38 -    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
    1.39 +    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
    1.40    | fn_lg (t as Var(f,tp)) (lg,seen) =
    1.41 -    if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
    1.42 -    else (lg,t ins seen)
    1.43 +    if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen)
    1.44    | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
    1.45    | fn_lg f _ = raise FN_LG(f); 
    1.46  
    1.47 @@ -256,7 +258,7 @@
    1.48      let val (f,args) = strip_comb tm
    1.49  	val (lg',seen') = if f mem seen then (FOL,seen) 
    1.50  			  else fn_lg f (FOL,seen)
    1.51 -
    1.52 +	val _ = if is_fol_logic lg' then () else warning ("Found a HOL term: " ^ (Term.str_of_term f))
    1.53  	 in
    1.54  	     term_lg (args@tms) (lg',seen')
    1.55      end
    1.56 @@ -265,9 +267,9 @@
    1.57  exception PRED_LG of term;
    1.58  
    1.59  fun pred_lg (t as Const(P,tp)) (lg,seen)= 
    1.60 -    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
    1.61 +    if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
    1.62    | pred_lg (t as Free(P,tp)) (lg,seen) =
    1.63 -    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
    1.64 +    if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
    1.65    | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
    1.66    | pred_lg P _ = raise PRED_LG(P);
    1.67