1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Oct 17 23:10:25 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 18 15:08:38 2005 +0200
     1.3 @@ -65,9 +65,9 @@
     1.4    | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
     1.5  
     1.6  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
     1.7 -fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
     1.8 +fun tptp_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) =
     1.9    let
    1.10 -    val clss = ResClause.make_conjecture_clauses thms
    1.11 +    val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.12      val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.13      val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    1.14      val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.15 @@ -80,8 +80,8 @@
    1.16    end;
    1.17  
    1.18  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.19 -fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.20 -    let val clss = ResClause.make_conjecture_clauses thms
    1.21 +fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.22 +    let val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.23          (*FIXME: classrel_clauses and arity_clauses*)
    1.24          val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
    1.25                          axclauses [] [] []    
    1.26 @@ -91,10 +91,7 @@
    1.27      end;
    1.28  
    1.29  
    1.30 -(*********************************************************************)
    1.31  (* call prover with settings and problem file for the current subgoal *)
    1.32 -(*********************************************************************)
    1.33 -(* now passing in list of skolemized thms and list of sgterms to go with them *)
    1.34  fun watcher_call_provers sign sg_terms (childin, childout, pid) =
    1.35    let
    1.36      fun make_atp_list [] n = []

     2.1 --- a/src/HOL/Tools/res_clause.ML	Mon Oct 17 23:10:25 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Oct 18 15:08:38 2005 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4    type clause
     2.5    val init : theory -> unit
     2.6    val make_axiom_clause : Term.term -> string * int -> clause
     2.7 -  val make_conjecture_clauses : thm list -> clause list
     2.8 +  val make_conjecture_clauses : term list -> clause list
     2.9    val get_axiomName : clause ->  string
    2.10    val isTaut : clause -> bool
    2.11    val num_of_clauses : clause -> int
    2.12 @@ -401,7 +401,7 @@
    2.13  	  val (ts2,ffuncs) = ListPair.unzip ts_funcs
    2.14  	  val ts3 = union_all (ts1::ts2)
    2.15  	  val ffuncs' = union_all ffuncs
    2.16 -	  val newfuncs = distinct (pfuncs@ffuncs')
    2.17 +	  val newfuncs = pfuncs union ffuncs'
    2.18  	  val arity = 
    2.19  	    case pred of
    2.20  		Const (c,_) => 
    2.21 @@ -423,25 +423,21 @@
    2.22    | predicate_of (term,polarity,tag) =
    2.23          (pred_of (strip_comb term), polarity, tag);
    2.24  
    2.25 -fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) =    
    2.26 -      literals_of_term(P,lits_ts, preds, funcs)
    2.27 -  | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = 
    2.28 -      let val (lits',ts', preds', funcs') = 
    2.29 -            literals_of_term(P,(lits,ts), preds,funcs)
    2.30 +fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
    2.31 +  | literals_of_term1 (args as (lits, ts, preds, funcs)) (Const("op |",_) $ P $ Q) = 
    2.32 +      let val (lits', ts', preds', funcs') = literals_of_term1 args P
    2.33        in
    2.34 -	  literals_of_term(Q, (lits',ts'), distinct(preds'@preds), 
    2.35 -	                   distinct(funcs'@funcs))
    2.36 +	  literals_of_term1 (lits', ts', preds' union preds, funcs' union funcs) Q
    2.37        end
    2.38 -  | literals_of_term (P,(lits,ts), preds, funcs) = 
    2.39 -      let val ((pred,ts', preds', funcs'), pol, tag) = 
    2.40 -              predicate_of (P,true,false)
    2.41 +  | literals_of_term1 (lits, ts, preds, funcs) P =
    2.42 +      let val ((pred, ts', preds', funcs'), pol, tag) = predicate_of (P,true,false)
    2.43  	  val lits' = Literal(pol,pred,tag) :: lits
    2.44        in
    2.45 -	  (lits', ts union ts', distinct(preds'@preds), distinct(funcs'@funcs))
    2.46 +	  (lits', ts union ts', preds' union preds, funcs' union funcs)
    2.47        end;
    2.48  
    2.49  
    2.50 -fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []);
    2.51 +val literals_of_term = literals_of_term1 ([],[],[],[]);
    2.52  
    2.53  
    2.54  (* FIX: not sure what to do with these funcs *)
    2.55 @@ -495,16 +491,15 @@
    2.56  fun get_tvar_strs [] = []
    2.57    | get_tvar_strs ((FOLTVar indx,s)::tss) = 
    2.58        let val vstr = make_schematic_type_var indx
    2.59 -          val vstrs = get_tvar_strs tss
    2.60        in
    2.61 -	  (distinct( vstr:: vstrs))
    2.62 +	  vstr ins (get_tvar_strs tss)
    2.63        end
    2.64    | get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss)
    2.65  
    2.66  (* FIX add preds and funcs to add typs aux here *)
    2.67  
    2.68  fun make_axiom_clause_thm thm (ax_name,cls_id) =
    2.69 -    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
    2.70 +    let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm)
    2.71  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
    2.72          val tvars = get_tvar_strs types_sorts
    2.73      in 
    2.74 @@ -515,8 +510,8 @@
    2.75  
    2.76  
    2.77  
    2.78 -fun make_conjecture_clause n thm =
    2.79 -    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
    2.80 +fun make_conjecture_clause n t =
    2.81 +    let val (lits,types_sorts, preds, funcs) = literals_of_term t
    2.82  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
    2.83          val tvars = get_tvar_strs types_sorts
    2.84      in
    2.85 @@ -526,14 +521,14 @@
    2.86      end;
    2.87      
    2.88  fun make_conjecture_clauses_aux _ [] = []
    2.89 -  | make_conjecture_clauses_aux n (th::ths) =
    2.90 -      make_conjecture_clause n th :: make_conjecture_clauses_aux (n+1) ths
    2.91 +  | make_conjecture_clauses_aux n (t::ts) =
    2.92 +      make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts
    2.93  
    2.94  val make_conjecture_clauses = make_conjecture_clauses_aux 0
    2.95  
    2.96  
    2.97  fun make_axiom_clause term (ax_name,cls_id) =
    2.98 -    let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[])
    2.99 +    let val (lits,types_sorts, preds,funcs) = literals_of_term term
   2.100  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
   2.101          val tvars = get_tvar_strs types_sorts	
   2.102      in 
   2.103 @@ -900,8 +895,8 @@
   2.104  	 val ax_name = get_axiomName cls
   2.105  	 val vars = dfg_vars cls
   2.106  	 val tvars = dfg_tvars cls
   2.107 -	 val funcs' = distinct((funcs_of_cls cls)@funcs)
   2.108 -	 val preds' = distinct((preds_of_cls cls)@preds)
   2.109 +	 val funcs' = (funcs_of_cls cls) union funcs
   2.110 +	 val preds' = (preds_of_cls cls) union preds
   2.111  	 val knd = string_of_kind cls
   2.112  	 val lits_str = concat_with ", " lits
   2.113  	 val axioms' = if knd = "axiom" then (cls::axioms) else axioms