src/HOL/Tools/meson.ML

   val meson_tac		: int -> tactic
   val negate_head	: thm -> thm
   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
 
 
 structure Meson =
 struct

         has_bool_arg_const prop  orelse  
         has_meta_conn prop
   then raise THM ("check_is_fol", 0, [th]) else th
   end;
 
+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;
+
+
 (*Create a meta-level Horn clause*)
 fun make_horn crules th = make_horn crules (tryres(th,crules))
 			  handle THM _ => th;
 
 (*Generate Horn clauses for all contrapositives of a clause. The input, th,

 val tag_False = thm "tag_False";
 val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
 val nnf_ss = HOL_basic_ss addsimps nnf_simps@simp_thms;
 
 fun make_nnf th = th |> simplify nnf_ss
-                     |> check_is_fol |> make_nnf1
+                     |> make_nnf1
 
 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   clauses that arise from a subgoal.*)
 fun skolemize th =
   if not (has_consts ["Ex"] (prop_of th)) then th

   expressed as a tactic (or Isar method).  Each assumption of the selected 
   goal is converted to NNF and then its existential quantifiers are pulled
   to the front. Finally, all existential quantifiers are eliminated, 
   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
 	    (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);
+
+
 
 (*Top-level conversion to meta-level clauses. Each clause has  
   leading !!-bound universal variables, to express generality. To get 
   disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
 val make_clauses_tac =