# HG changeset patch
# User nipkow
# Date 1245697173 -7200
# Node ID 78529fc872b10998f50632193c3101b35682f062
# Parent  a61475260e479ac6a87b580abee02ecbc0ce4751# Parent  b5260f5272a482f609629272fc08adfa8ba85967
merged

diff -r b5260f5272a4 -r 78529fc872b1 doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Mon Jun 22 20:59:12 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Mon Jun 22 20:59:33 2009 +0200
@@ -143,8 +143,8 @@
 
 interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-    and nat_dvd_meet_eq: "lattice.meet op dvd = gcd"
-    and nat_dvd_join_eq: "lattice.join op dvd = lcm"
+    and nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+    and nat_dvd_join_eq: "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
 proof -
   show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     apply unfold_locales
@@ -152,23 +152,24 @@
     apply (rule_tac x = "gcd x y" in exI)
     apply auto [1]
     apply (rule_tac x = "lcm x y" in exI)
-    apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
+    apply (auto intro: nat_lcm_least)
     done
   then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
   show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
     by (rule nat_dvd_less_eq)
-  show "lattice.meet op dvd = gcd"
+  show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
     apply (auto simp add: expand_fun_eq)
     apply (unfold nat_dvd.meet_def)
     apply (rule the_equality)
     apply (unfold nat_dvd.is_inf_def)
     by auto
-  show "lattice.join op dvd = lcm"
+  show "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
     apply (auto simp add: expand_fun_eq)
     apply (unfold nat_dvd.join_def)
     apply (rule the_equality)
     apply (unfold nat_dvd.is_sup_def)
-    by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
+    apply (auto intro: nat_lcm_least iff: nat_lcm_unique)
+    done
 qed
 
 text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
@@ -198,8 +199,8 @@
 interpretation %visible nat_dvd:
   distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
   where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
-    and "lattice.meet op dvd = gcd"
-    and "lattice.join op dvd = lcm"
+    and "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+    and "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
 proof -
   show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
     apply unfold_locales
diff -r b5260f5272a4 -r 78529fc872b1 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Mon Jun 22 20:59:12 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Mon Jun 22 20:59:33 2009 +0200
@@ -307,8 +307,8 @@
 \isacommand{interpretation}\isamarkupfalse%
 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
 %
 \isadelimproof
 %
@@ -330,7 +330,7 @@
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{done}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{then}\isamarkupfalse%
@@ -342,7 +342,7 @@
 \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
@@ -354,7 +354,7 @@
 \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ auto\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
@@ -363,8 +363,10 @@
 \ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{apply}\isamarkupfalse%
 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least\ iff{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}unique{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{done}\isamarkupfalse%
+\isanewline
 \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
@@ -407,8 +409,8 @@
 \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
 \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{show}\isamarkupfalse%
diff -r b5260f5272a4 -r 78529fc872b1 src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Mon Jun 22 20:59:33 2009 +0200
@@ -20,9 +20,9 @@
   val info: unit -> unit
   val messages: int option -> unit
   type prover = int -> (thm * (string * int)) list option ->
-    (int Symtab.table * bool Symtab.table) option -> string -> int ->
+    (thm * (string * int)) list option -> string -> int ->
     Proof.context * (thm list * thm) ->
-    bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
+    bool * string * string * string vector * (thm * (string * int)) list
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
   val get_prover: string -> theory -> prover option
@@ -292,9 +292,9 @@
 (* named provers *)
 
 type prover = int -> (thm * (string * int)) list option ->
-  (int Symtab.table * bool Symtab.table) option -> string -> int ->
+  (thm * (string * int)) list option -> string -> int ->
   Proof.context * (thm list * thm) ->
-  bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
+  bool * string * string * string vector * (thm * (string * int)) list
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
diff -r b5260f5272a4 -r 78529fc872b1 src/HOL/Tools/atp_minimal.ML
--- a/src/HOL/Tools/atp_minimal.ML	Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/atp_minimal.ML	Mon Jun 22 20:59:33 2009 +0200
@@ -83,9 +83,9 @@
    ("# Cannot determine problem status within resource limit", Timeout),
    ("Error", Error)]
 
-fun produce_answer (success, message, result_string, thm_name_vec, const_counts) =
+fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
   if success then
-    (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string)
+    (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
   else
     let
       val failure = failure_strings |> get_first (fn (s, t) =>
@@ -100,7 +100,7 @@
 
 (* wrapper for calling external prover *)
 
-fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs =
+fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
   let
     val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
     val name_thm_pairs =
@@ -109,7 +109,7 @@
     val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     val (result, proof) =
       produce_answer
-        (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state))
+        (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
     val _ = println (string_of_result result)
     val _ = debug proof
   in
@@ -127,11 +127,12 @@
     val _ = debug_fn (fn () => app (fn (n, tl) =>
         (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
     val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
-    fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false
+    fun test_thms filtered thms =
+      case test_thms_fun filtered thms of (Success _, _) => true | _ => false
   in
     (* try prove first to check result and get used theorems *)
     (case test_thms_fun NONE name_thms_pairs of
-      (Success (used, const_counts), _) =>
+      (Success (used, filtered), _) =>
         let
           val ordered_used = order_unique used
           val to_use =
@@ -139,7 +140,7 @@
               filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
             else
               name_thms_pairs
-          val min_thms = (minimal (test_thms (SOME const_counts)) to_use)
+          val min_thms = (minimal (test_thms (SOME filtered)) to_use)
           val min_names = order_unique (map fst min_thms)
           val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
           val _ = debug_fn (fn () => print_names min_thms)
diff -r b5260f5272a4 -r 78529fc872b1 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 20:59:33 2009 +0200
@@ -41,7 +41,7 @@
 (* basic template *)
 
 fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
-  timeout axiom_clauses const_counts name subgoalno goal =
+  timeout axiom_clauses filtered_clauses name subgoalno goal =
   let
     (* path to unique problem file *)
     val destdir' = ! destdir
@@ -54,37 +54,40 @@
         else error ("No such directory: " ^ destdir')
       end
 
-    (* write out problem file and call prover *)
+    (* get clauses and prepare them for writing *)
     val (ctxt, (chain_ths, th)) = goal
     val thy = ProofContext.theory_of ctxt
     val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
-    val probfile = prob_pathname subgoalno
-    val fname = File.platform_path probfile
     val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
       handle THM ("assume: variables", _, _) =>
         error "Sledgehammer: Goal contains type variables (TVars)"
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+    val the_filtered_clauses =
+      case filtered_clauses of
+          NONE => relevance_filter goal goal_cls
+        | SOME fcls => fcls
     val the_axiom_clauses =
       case axiom_clauses of
-          NONE => relevance_filter goal goal_cls
+          NONE => the_filtered_clauses
         | SOME axcls => axcls
-    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy
-    val the_const_counts = case const_counts of
-      NONE =>
-        ResHolClause.count_constants(
-          case axiom_clauses of
-            NONE => clauses
-            | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy)
-          )
-      | SOME ccs => ccs
-    val _ = writer fname the_const_counts clauses
+    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
+
+    (* write out problem file and call prover *)
+    val probfile = prob_pathname subgoalno
+    val fname = File.platform_path probfile
+    val _ = writer fname clauses
     val cmdline =
       if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
       else error ("Bad executable: " ^ Path.implode cmd)
     val (proof, rc) = system_out (cmdline ^ " " ^ fname)
 
-    (* remove *temporary* files *)
-    val _ = if destdir' = "" then OS.FileSys.remove fname else ()
+    (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
+    val _ =
+      if destdir' = "" then OS.FileSys.remove fname
+      else
+        let val out = TextIO.openOut (fname ^ "_proof")
+        val _ = TextIO.output (out, proof)
+        in TextIO.closeOut out end
     
     (* check for success and print out some information on failure *)
     val failure = find_failure proof
@@ -94,7 +97,7 @@
       else if rc <> 0 then "External prover failed: " ^ proof
       else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
     val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
-  in (success, message, proof, thm_names, the_const_counts) end;
+  in (success, message, proof, thm_names, the_filtered_clauses) end;
 
 
 
@@ -102,7 +105,7 @@
 
 (* generic TPTP-based provers *)
 
-fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal =
+fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
   external_prover
   (ResAtp.get_relevant max_new theory_const)
   (ResAtp.prepare_clauses false)
@@ -110,7 +113,7 @@
   command
   ResReconstruct.find_failure
   (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
-  timeout ax_clauses ccs name n goal;
+  timeout ax_clauses fcls name n goal;
 
 (*arbitrary ATP with TPTP input/output and problemfile as last argument*)
 fun tptp_prover_opts max_new theory_const =
@@ -167,7 +170,7 @@
 
 (* SPASS *)
 
-fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover
+fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
   (ResAtp.get_relevant max_new theory_const)
   (ResAtp.prepare_clauses true)
   ResHolClause.dfg_write_file
@@ -175,7 +178,7 @@
     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
   ResReconstruct.find_failure
   ResReconstruct.lemma_list_dfg
-  timeout ax_clauses ccs name n goal;
+  timeout ax_clauses fcls name n goal;
 
 val spass = spass_opts 40 true;
 
diff -r b5260f5272a4 -r 78529fc872b1 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Jun 22 20:59:33 2009 +0200
@@ -9,6 +9,7 @@
   val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
     (thm * (string * int)) list
   val prepare_clauses : bool -> thm list -> thm list ->
+    (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
     ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
     ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
@@ -526,26 +527,30 @@
     relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
   end;
 
-(* prepare and count clauses before writing *)
-fun prepare_clauses dfg goal_cls chain_ths axcls thy =
+(* prepare for passing to writer,
+   create additional clauses based on the information from extra_cls *)
+fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
-    val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
+    val white_thms =
+      filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
     val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
-    val axcls = white_cls @ axcls
-    val ccls = subtract_cls goal_cls axcls
+    val extra_cls = white_cls @ extra_cls
+    val ccls = subtract_cls goal_cls extra_cls
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
     val ccltms = map prop_of ccls
-    and axtms = map (prop_of o #1) axcls
+    and axtms = map (prop_of o #1) extra_cls
     val subs = tfree_classes_of_terms ccltms
     and supers = tvar_classes_of_terms axtms
     and tycons = type_consts_of_terms thy (ccltms@axtms)
     (*TFrees in conjecture clauses; TVars in axiom clauses*)
-    val (clnames, (conjectures, axiom_clauses, helper_clauses)) =
-      ResHolClause.prepare_clauses dfg thy (isFO thy goal_cls) ccls axcls []
+    val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
+    val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
+    val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, [])
     val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
     val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   in
-    (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
+    (Vector.fromList clnames,
+      (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
   end
 
 end;
diff -r b5260f5272a4 -r 78529fc872b1 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Mon Jun 22 20:59:33 2009 +0200
@@ -28,13 +28,18 @@
   val strip_comb: combterm -> combterm * combterm list
   val literals_of_term: theory -> term -> literal list * typ list
   exception TOO_TRIVIAL
-  val count_constants: clause list * clause list * clause list * 'a * 'b ->
-    int Symtab.table * bool Symtab.table
-  val prepare_clauses: bool -> theory -> bool -> thm list -> (thm * (axiom_name * clause_id)) list ->
-    string list -> axiom_name list * (clause list * clause list * clause list)
-  val tptp_write_file: string -> int Symtab.table * bool Symtab.table ->
+  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list (* dfg thy ccls *)
+  val make_axiom_clauses: bool ->
+       theory ->
+       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
+  val get_helper_clauses: bool ->
+       theory ->
+       bool ->
+       clause list * (thm * (axiom_name * clause_id)) list * string list ->
+       clause list
+  val tptp_write_file: string ->
     clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
-  val dfg_write_file: string -> int Symtab.table * bool Symtab.table ->
+  val dfg_write_file: string -> 
     clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
 end
 
@@ -403,10 +408,12 @@
 fun cnf_helper_thms thy =
   ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
 
-fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) =
+fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   if isFO then []  (*first-order*)
   else
-    let val ct0 = List.foldl count_clause init_counters conjectures
+    let
+        val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
+        val ct0 = List.foldl count_clause init_counters conjectures
         val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
         fun needed c = valOf (Symtab.lookup ct c) > 0
         val IK = if needed "c_COMBI" orelse needed "c_COMBK"
@@ -464,18 +471,10 @@
 
 (* tptp format *)
 
-fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas =
+fun tptp_write_file filename clauses =
   let
-    val conjectures = make_conjecture_clauses dfg thy thms
-    val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses dfg thy ax_tuples)
-    val helper_clauses = get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas)
-  in
-    (clnames, (conjectures, axclauses, helper_clauses))
-  end
-
-(* write TPTP format to a single file *)
-fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
-  let
+    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val const_counts = count_constants clauses
     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures)
     val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
     val out = TextIO.openOut filename
@@ -492,8 +491,10 @@
 
 (* dfg format *)
 
-fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
+fun dfg_write_file filename clauses =
   let
+    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val const_counts = count_constants clauses
     val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures)
     and probname = Path.implode (Path.base (Path.explode filename))
     val axstrs = map (#1 o (clause2dfg const_counts)) axclauses
diff -r b5260f5272a4 -r 78529fc872b1 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Mon Jun 22 20:59:12 2009 +0200
+++ b/src/Pure/General/scan.scala	Mon Jun 22 20:59:33 2009 +0200
@@ -19,11 +19,8 @@
     private case class Tree(val branches: Map[Char, (String, Tree)])
     private val empty_tree = Tree(Map())
 
-    private def make(tree: Tree, max: Int): Lexicon =
-      new Lexicon {
-        override val main_tree = tree
-        override val max_entry = max
-      }
+    private def make(tree: Tree): Lexicon =
+      new Lexicon { override val main_tree = tree }
 
     val empty: Lexicon = new Lexicon
     def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str)
@@ -35,7 +32,6 @@
 
     import Lexicon.Tree
     val main_tree: Tree = Lexicon.empty_tree
-    val max_entry = -1
 
 
     /* auxiliary operations */
@@ -74,7 +70,7 @@
 
     override def stringPrefix = "Lexicon"
 
-    override def isEmpty: Boolean = { max_entry < 0 }
+    override def isEmpty: Boolean = { main_tree.branches.isEmpty }
 
     def size: Int = content(main_tree, Nil).length
     def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
@@ -102,7 +98,7 @@
         } else tree
       }
       if (contains(str)) this
-      else Lexicon.make(extend(main_tree, 0), max_entry max str.length)
+      else Lexicon.make(extend(main_tree, 0))
     }
 
     def empty[A]: Set[A] = error("Undefined")