# HG changeset patch
# User paulson
# Date 1141746304 -3600
# Node ID b8f7de7ef6296553c5b28241f3cdecfce7fc76ca
# Parent  7785075206842dd29075f7737a84677e5bf90478
Tidying, and getting rid of SELECT_GOAL (as it does something different now)

diff -r 778507520684 -r b8f7de7ef629 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Mar 07 16:03:31 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Tue Mar 07 16:45:04 2006 +0100
@@ -36,7 +36,6 @@
   val select_literal	: int -> thm -> thm
   val skolemize_tac	: int -> tactic
   val make_clauses_tac	: int -> tactic
-  val check_is_fol : thm -> thm
   val check_is_fol_term : term -> term
 end
 
@@ -289,12 +288,15 @@
 (*Raises an exception if any Vars in the theorem mention type bool; they
   could cause make_horn to loop! Also rejects functions whose arguments are 
   Booleans or other functions.*)
-fun check_is_fol_term term =
-    if exists (has_bool o fastype_of) (term_vars term)  orelse
-        not (Term.is_first_order ["all","All","Ex"] term) orelse
-        has_bool_arg_const term  orelse  
-        has_meta_conn term
-    then raise TERM("check_is_fol_term",[term]) else term;
+fun is_fol_term t =
+    not (exists (has_bool o fastype_of) (term_vars t)  orelse
+	 not (Term.is_first_order ["all","All","Ex"] t) orelse
+	 has_bool_arg_const t  orelse  
+	 has_meta_conn t);
+
+(*FIXME: replace this by the boolean-valued version above!*)
+fun check_is_fol_term t =
+    if is_fol_term t then t else raise TERM("check_is_fol_term",[t]);
 
 fun check_is_fol th = (check_is_fol_term (prop_of th); th);
 
@@ -548,17 +550,15 @@
   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   might generate many subgoals.*)
 
-val skolemize_tac = 
-  SUBGOAL
-    (fn (prop,_) =>
-     let val ts = Logic.strip_assums_hyp prop
-     in EVERY1 
-	 [METAHYPS
+fun skolemize_tac i st = 
+  let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
+  in 
+     EVERY' [METAHYPS
 	    (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
                          THEN REPEAT (etac exE 1))),
-	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
-     end);
-
+            REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
+  end
+  handle Subscript => Seq.empty;
 
 (*Top-level conversion to meta-level clauses. Each clause has  
   leading !!-bound universal variables, to express generality. To get