# HG changeset patch
# User paulson
# Date 1172835538 -3600
# Node ID 01e90256550d562337661bbfcba8fd06385a55be
# Parent  dbf09db0a40d62c7851fd398a5ec11d6528dd341
Meson.is_fol_term now takes a theory as argument. Minor tidying.

diff -r dbf09db0a40d -r 01e90256550d src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Mar 02 12:37:34 2007 +0100
+++ b/src/HOL/Tools/res_clause.ML	Fri Mar 02 12:38:58 2007 +0100
@@ -412,7 +412,8 @@
 
 (* check if a clause is first-order before making a conjecture clause*)
 fun make_conjecture_clause n th =
-  if Meson.is_fol_term (prop_of th) then make_clause(n, "conjecture", th, Conjecture)
+  if Meson.is_fol_term (theory_of_thm th) (prop_of th) 
+  then make_clause(n, "conjecture", th, Conjecture)
   else raise CLAUSE("Goal is not FOL", prop_of th);
   
 fun make_conjecture_clauses_aux _ [] = []
@@ -422,14 +423,14 @@
 val make_conjecture_clauses = make_conjecture_clauses_aux 0
 
 (*before converting an axiom clause to "clause" format, check if it is FOL*)
-fun make_axiom_clause thm (ax_name,cls_id) =
-  if Meson.is_fol_term (prop_of thm) 
-  then (SOME (make_clause(cls_id, ax_name, thm, Axiom)) handle MAKE_CLAUSE => NONE)
+fun make_axiom_clause th (ax_name,cls_id) =
+  if Meson.is_fol_term (theory_of_thm th) (prop_of th) 
+  then (SOME (make_clause(cls_id, ax_name, th, Axiom)) handle MAKE_CLAUSE => NONE)
   else (Output.debug (fn () => ("Omitting " ^ ax_name ^ ": Axiom is not FOL")); NONE)
     
 fun make_axiom_clauses [] = []
-  | make_axiom_clauses ((thm,(name,id))::thms) =
-      case make_axiom_clause thm (name,id) of 
+  | make_axiom_clauses ((th,(name,id))::thms) =
+      case make_axiom_clause th (name,id) of 
           SOME cls => if isTaut cls then make_axiom_clauses thms 
                       else (name,cls) :: make_axiom_clauses thms
         | NONE => make_axiom_clauses thms;