Tidied up some programs.

--- a/src/HOL/Tools/res_atp.ML	Sun Apr 16 08:22:29 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Apr 18 05:36:38 2006 +0200
@@ -313,18 +313,6 @@
     end
   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
 
-fun logic_of_nclauses [] (lg,seen) = (lg,seen)
-  | logic_of_nclauses (cls::clss) (FOL,seen) =
-    logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
-  | logic_of_nclauses clss (lg,seen) = (lg,seen);
-
-fun problem_logic (goal_cls,rules_cls) =
-    let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[])
-	val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1)
-    in
-	lg2
-    end;
-
 fun problem_logic_goals_aux [] (lg,seen) = lg
   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
@@ -360,13 +348,13 @@
 
 
 fun write_subgoal_file mode ctxt conjectures user_thms n =
-    let val conj_cls = map prop_of (make_clauses conjectures) 
-	val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
+    let val conj_cls = make_clauses conjectures 
+	val hyp_cls = cnf_hyps_thms ctxt
 	val goal_cls = conj_cls@hyp_cls
 	val user_rules = map ResAxioms.pairname user_thms
-	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
+	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (map prop_of goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
 	val thy = ProofContext.theory_of ctxt
-	val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
+	val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
 				    | Fol => FOL
 				    | Hol => HOL
 	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
@@ -465,7 +453,7 @@
 fun write_problem_files pf (ctxt,th)  =
   let val goals = Thm.prems_of th
       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
-      val (names_arr, axclauses_as_terms) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
+      val (names_arr, axclauses) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
       val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
                      Int.toString (Array.length names_arr))
       val thy = ProofContext.theory_of ctxt
@@ -475,12 +463,12 @@
 	      let val st = Seq.hd (EVERY'
 				       [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th)
 		  val negs = Option.valOf (metahyps_thms n st)
-		  val negs_clauses = map prop_of (make_clauses negs)
+		  val negs_clauses = make_clauses negs
 	      in
 		  negs_clauses::(get_neg_subgoals (n - 1))
 	      end
       val neg_subgoals = get_neg_subgoals (length goals) 
-      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals neg_subgoals
+      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
 						 | Fol => FOL
 						 | Hol => HOL
       val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
@@ -491,7 +479,7 @@
       val writer = (*if !prover ~= "spass" then *)tptp_writer 
       fun write_all [] _ = []
 	| write_all (subgoal::subgoals) k =
-	  (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
+	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
   in
       (write_all neg_subgoals (length goals), names_arr)
   end;

--- a/src/HOL/Tools/res_axioms.ML	Sun Apr 16 08:22:29 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Apr 18 05:36:38 2006 +0200
@@ -12,22 +12,15 @@
   val elimRule_tac : thm -> Tactical.tactic
   val elimR2Fol : thm -> term
   val transform_elim : thm -> thm
-  val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
-  val clausify_axiom_pairsH : (string*thm) -> (ResHolClause.clause*thm) list
   val cnf_axiom : (string * thm) -> thm list
   val meta_cnf_axiom : thm -> thm list
   val claset_rules_of_thy : theory -> (string * thm) list
   val simpset_rules_of_thy : theory -> (string * thm) list
   val claset_rules_of_ctxt: Proof.context -> (string * thm) list
   val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
-  val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
-  val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list
   val pairname : thm -> (string * thm)
   val skolem_thm : thm -> thm list
-  val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
-  val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
   val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
-  val clausify_rules_pairs_abs : (string * thm) list -> (Term.term * (string * int)) list list
   val meson_method_setup : theory -> theory
   val setup : theory -> theory
 
@@ -391,19 +384,6 @@
 (*works for both FOL and HOL*)
 val cnf_rules = cnf_rules_g cnf_axiom;
 
-fun cnf_rules1 [] err_list = ([],err_list)
-  | cnf_rules1 ((name,th) :: ths) err_list =
-      let val (ts,es) = cnf_rules1 ths err_list
-      in ((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end;
-
-fun cnf_rules2 [] err_list = ([],err_list)
-  | cnf_rules2 ((name,th) :: ths) err_list =
-      let val (ts,es) = cnf_rules2 ths err_list
-      in
-	((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) 
-      end;
-
-
 fun cnf_rules_pairs_aux [] = []
   | cnf_rules_pairs_aux ((name,th)::ths) =
     let val ts = cnf_rules_pairs_aux ths
@@ -418,70 +398,9 @@
 
 fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms);
 
-fun clausify_rules_pairs_abs_aux [] = []
-  | clausify_rules_pairs_abs_aux ((name,th)::ths) =
-      let val ts = clausify_rules_pairs_abs_aux ths
-	  fun pair_name_cls k (n, []) = []
-	    | pair_name_cls k (n, cls::clss) =
-		(prop_of cls, (n,k)) :: (pair_name_cls (k+1) (n, clss))
-      in
-	  pair_name_cls 0 (name, (cnf_axiom(name,th))) :: ts
-	  handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts
-      end;
-
-fun clausify_rules_pairs_abs thms = rev (clausify_rules_pairs_abs_aux thms);
-
 
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
 
-fun make_axiom_clauses _ _ [] = []
-  | make_axiom_clauses name i (th::ths) =
-      case ResClause.make_axiom_clause (prop_of th) (name,i) of 
-          SOME cls => (cls, th) :: make_axiom_clauses name (i+1) ths
-        | NONE => make_axiom_clauses name i ths;
-
-(* outputs a list of (clause,theorem) pairs *)
-fun clausify_axiom_pairs (name,th) = 
-    filter (fn (c,th) => not (ResClause.isTaut c))
-           (make_axiom_clauses name 0 (cnf_axiom (name,th)));
-
-fun make_axiom_clausesH _ _ [] = []
-  | make_axiom_clausesH name i (th::ths) =
-      (ResHolClause.make_axiom_clause (prop_of th) (name,i), th) ::
-      (make_axiom_clausesH name (i+1) ths)
-
-fun clausify_axiom_pairsH (name,th) = 
-    filter (fn (c,th) => not (ResHolClause.isTaut c))
-           (make_axiom_clausesH name 0 (cnf_axiom (name,th)));
-
-
-fun clausify_rules_pairs_aux result [] = result
-  | clausify_rules_pairs_aux result ((name,th)::ths) =
-      clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths
-      handle THM (msg,_,_) =>  
-	      (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
-	       clausify_rules_pairs_aux result ths)
-	 |  ResClause.CLAUSE (msg,t) => 
-	      (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg ^
-		      ": " ^ TermLib.string_of_term t); 
-	       clausify_rules_pairs_aux result ths)
-
-
-fun clausify_rules_pairs_auxH result [] = result
-  | clausify_rules_pairs_auxH result ((name,th)::ths) =
-      clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths
-      handle THM (msg,_,_) =>  
-	      (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
-	       clausify_rules_pairs_auxH result ths)
-	 |  ResHolClause.LAM2COMB (t) => 
-	      (Output.debug ("Cannot clausify "  ^ TermLib.string_of_term t); 
-	       clausify_rules_pairs_auxH result ths)
-
-
-
-val clausify_rules_pairs = clausify_rules_pairs_aux [];
-
-val clausify_rules_pairsH = clausify_rules_pairs_auxH [];
 
 (*These should include any plausibly-useful theorems, especially if they need
   Skolem functions. FIXME: this list is VERY INCOMPLETE*)