1.1 --- a/src/HOL/Tools/meson.ML	Tue Mar 07 16:03:31 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Mar 07 16:45:04 2006 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4    val select_literal	: int -> thm -> thm
     1.5    val skolemize_tac	: int -> tactic
     1.6    val make_clauses_tac	: int -> tactic
     1.7 -  val check_is_fol : thm -> thm
     1.8    val check_is_fol_term : term -> term
     1.9  end
    1.10  
    1.11 @@ -289,12 +288,15 @@
    1.12  (*Raises an exception if any Vars in the theorem mention type bool; they
    1.13    could cause make_horn to loop! Also rejects functions whose arguments are 
    1.14    Booleans or other functions.*)
    1.15 -fun check_is_fol_term term =
    1.16 -    if exists (has_bool o fastype_of) (term_vars term)  orelse
    1.17 -        not (Term.is_first_order ["all","All","Ex"] term) orelse
    1.18 -        has_bool_arg_const term  orelse  
    1.19 -        has_meta_conn term
    1.20 -    then raise TERM("check_is_fol_term",[term]) else term;
    1.21 +fun is_fol_term t =
    1.22 +    not (exists (has_bool o fastype_of) (term_vars t)  orelse
    1.23 +	 not (Term.is_first_order ["all","All","Ex"] t) orelse
    1.24 +	 has_bool_arg_const t  orelse  
    1.25 +	 has_meta_conn t);
    1.26 +
    1.27 +(*FIXME: replace this by the boolean-valued version above!*)
    1.28 +fun check_is_fol_term t =
    1.29 +    if is_fol_term t then t else raise TERM("check_is_fol_term",[t]);
    1.30  
    1.31  fun check_is_fol th = (check_is_fol_term (prop_of th); th);
    1.32  
    1.33 @@ -548,17 +550,15 @@
    1.34    leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
    1.35    might generate many subgoals.*)
    1.36  
    1.37 -val skolemize_tac = 
    1.38 -  SUBGOAL
    1.39 -    (fn (prop,_) =>
    1.40 -     let val ts = Logic.strip_assums_hyp prop
    1.41 -     in EVERY1 
    1.42 -	 [METAHYPS
    1.43 +fun skolemize_tac i st = 
    1.44 +  let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
    1.45 +  in 
    1.46 +     EVERY' [METAHYPS
    1.47  	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
    1.48                           THEN REPEAT (etac exE 1))),
    1.49 -	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.50 -     end);
    1.51 -
    1.52 +            REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
    1.53 +  end
    1.54 +  handle Subscript => Seq.empty;
    1.55  
    1.56  (*Top-level conversion to meta-level clauses. Each clause has  
    1.57    leading !!-bound universal variables, to express generality. To get