src/HOL/Tools/res_clause.ML
changeset 20418 7c1aa7872266
parent 20038 73231d03a2ac
child 20422 35a6a4c863f1
     1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Aug 25 18:47:36 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Aug 25 18:48:09 2006 +0200
     1.3 @@ -440,14 +440,10 @@
     1.4    | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
     1.5  
     1.6  (* check if a clause is first-order before making a conjecture clause*)
     1.7 -fun make_conjecture_clause n thm =
     1.8 -    let val t = prop_of thm
     1.9 -	val _ = check_is_fol_term t
    1.10 -	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Goal is not FOL",t)
    1.11 -    in
    1.12 -	make_clause(n, "conjecture", thm, Conjecture)
    1.13 -    end;
    1.14 -    
    1.15 +fun make_conjecture_clause n th =
    1.16 +  if Meson.is_fol_term (prop_of th) then make_clause(n, "conjecture", th, Conjecture)
    1.17 +  else raise CLAUSE("Goal is not FOL", prop_of th);
    1.18 +  
    1.19  fun make_conjecture_clauses_aux _ [] = []
    1.20    | make_conjecture_clauses_aux n (t::ts) =
    1.21        make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts