# HG changeset patch
# User mengj
# Date 1132293911 -3600
# Node ID 940515d2fa2636d5ef8e84fde498a85b18487da5
# Parent  54419506df9e8b4c7cde906541f41896f92cf320
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
-- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input.
-- added "check_is_fol" and "check_is_fol_term" into the signature.

diff -r 54419506df9e -r 940515d2fa26 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Nov 16 19:34:19 2005 +0100
+++ b/src/HOL/Tools/meson.ML	Fri Nov 18 07:05:11 2005 +0100
@@ -36,6 +36,8 @@
   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
 
 
@@ -252,6 +254,14 @@
   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;
@@ -339,7 +349,7 @@
 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.*)
@@ -490,6 +500,9 @@
   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,_) =>
@@ -501,6 +514,8 @@
 	  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.*)