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