# HG changeset patch
# User paulson
# Date 1156524489 -7200
# Node ID 7c1aa787226618df3512fedcfcff11276437c59f
# Parent  c611b1412056c09a0afd695dcffa56295873c099
tidied

diff -r c611b1412056 -r 7c1aa7872266 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Aug 25 18:47:36 2006 +0200
+++ b/src/HOL/Tools/res_clause.ML	Fri Aug 25 18:48:09 2006 +0200
@@ -440,14 +440,10 @@
   | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
 
 (* check if a clause is first-order before making a conjecture clause*)
-fun make_conjecture_clause n thm =
-    let val t = prop_of thm
-	val _ = check_is_fol_term t
-	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
-    in
-	make_clause(n, "conjecture", thm, Conjecture)
-    end;
-    
+fun make_conjecture_clause n th =
+  if Meson.is_fol_term (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 _ [] = []
   | make_conjecture_clauses_aux n (t::ts) =
       make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts