renamed Sledgehammer structures
authorblanchet
Wed Mar 17 19:26:05 2010 +0100 (2010-03-17 ago)
changeset 358261590abc3d42a
parent 35825 a6aad5a70ed4
child 35827 f552152d7747
renamed Sledgehammer structures
src/HOL/ATP_Linkup.thy
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_minimal.ML
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Mar 17 18:16:31 2010 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Mar 17 19:26:05 2010 +0100
     1.3 @@ -92,10 +92,10 @@
     1.4  subsection {* Setup of external ATPs *}
     1.5  
     1.6  use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML"
     1.7 -setup Res_Axioms.setup
     1.8 +setup Sledgehammer_Fact_Preprocessor.setup
     1.9  use "Tools/Sledgehammer/sledgehammer_hol_clause.ML"
    1.10  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
    1.11 -setup Res_Reconstruct.setup
    1.12 +setup Sledgehammer_Proof_Reconstruct.setup
    1.13  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
    1.14  
    1.15  use "Tools/ATP_Manager/atp_wrapper.ML"
    1.16 @@ -125,6 +125,6 @@
    1.17  subsection {* The Metis prover *}
    1.18  
    1.19  use "Tools/Sledgehammer/metis_tactics.ML"
    1.20 -setup MetisTools.setup
    1.21 +setup Metis_Tactics.setup
    1.22  
    1.23  end
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Mar 17 18:16:31 2010 +0100
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Mar 17 19:26:05 2010 +0100
     2.3 @@ -263,7 +263,7 @@
     2.4              val _ = register birth_time death_time (Thread.self (), desc);
     2.5              val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
     2.6              val message = #message (prover (! timeout) problem)
     2.7 -              handle Res_HOL_Clause.TOO_TRIVIAL =>   (* FIXME !? *)
     2.8 +              handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>   (* FIXME !? *)
     2.9                    "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
    2.10                  | ERROR msg => ("Error: " ^ msg);
    2.11              val _ = unregister message (Thread.self ());
     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Mar 17 18:16:31 2010 +0100
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Mar 17 19:26:05 2010 +0100
     3.3 @@ -116,7 +116,7 @@
     3.4    let
     3.5      val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
     3.6      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     3.7 -    val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     3.8 +    val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     3.9      val {context = ctxt, facts, goal} = Proof.goal state
    3.10      val problem =
    3.11       {with_full_types = ! ATP_Manager.full_types,
    3.12 @@ -170,7 +170,7 @@
    3.13          (NONE, "Error in prover: " ^ msg)
    3.14      | (Failure, _) =>
    3.15          (NONE, "Failure: No proof with the theorems supplied"))
    3.16 -    handle Res_HOL_Clause.TOO_TRIVIAL =>
    3.17 +    handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
    3.18          (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
    3.19        | ERROR msg => (NONE, "Error: " ^ msg)
    3.20    end
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Mar 17 18:16:31 2010 +0100
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Mar 17 19:26:05 2010 +0100
     4.3 @@ -52,6 +52,9 @@
     4.4  structure ATP_Wrapper: ATP_WRAPPER =
     4.5  struct
     4.6  
     4.7 +structure SFF = Sledgehammer_Fact_Filter
     4.8 +structure SPR = Sledgehammer_Proof_Reconstruct
     4.9 +
    4.10  (** generic ATP wrapper **)
    4.11  
    4.12  (* external problem files *)
    4.13 @@ -117,8 +120,8 @@
    4.14      (* get clauses and prepare them for writing *)
    4.15      val (ctxt, (chain_ths, th)) = goal;
    4.16      val thy = ProofContext.theory_of ctxt;
    4.17 -    val chain_ths = map (Thm.put_name_hint Res_Reconstruct.chained_hint) chain_ths;
    4.18 -    val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoal);
    4.19 +    val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths;
    4.20 +    val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
    4.21      val the_filtered_clauses =
    4.22        (case filtered_clauses of
    4.23          NONE => relevance_filter goal goal_cls
    4.24 @@ -181,7 +184,7 @@
    4.25        with_path cleanup export run_on (prob_pathname subgoal);
    4.26  
    4.27      (* check for success and print out some information on failure *)
    4.28 -    val failure = Res_Reconstruct.find_failure proof;
    4.29 +    val failure = SPR.find_failure proof;
    4.30      val success = rc = 0 andalso is_none failure;
    4.31      val (message, real_thm_names) =
    4.32        if is_some failure then ("External prover failed.", [])
    4.33 @@ -203,13 +206,13 @@
    4.34        prover_config;
    4.35    in
    4.36      external_prover
    4.37 -      (Res_ATP.get_relevant max_new_clauses insert_theory_const)
    4.38 -      (Res_ATP.prepare_clauses false)
    4.39 -      Res_HOL_Clause.tptp_write_file
    4.40 +      (SFF.get_relevant max_new_clauses insert_theory_const)
    4.41 +      (SFF.prepare_clauses false)
    4.42 +      Sledgehammer_HOL_Clause.tptp_write_file
    4.43        command
    4.44        (arguments timeout)
    4.45 -      (if emit_structured_proof then Res_Reconstruct.structured_proof
    4.46 -       else Res_Reconstruct.lemma_list false)
    4.47 +      (if emit_structured_proof then SPR.structured_proof
    4.48 +       else SPR.lemma_list false)
    4.49        name
    4.50        problem
    4.51    end;
    4.52 @@ -274,12 +277,12 @@
    4.53      val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
    4.54    in
    4.55      external_prover
    4.56 -      (Res_ATP.get_relevant max_new_clauses insert_theory_const)
    4.57 -      (Res_ATP.prepare_clauses true)
    4.58 -      Res_HOL_Clause.dfg_write_file
    4.59 +      (SFF.get_relevant max_new_clauses insert_theory_const)
    4.60 +      (SFF.prepare_clauses true)
    4.61 +      Sledgehammer_HOL_Clause.dfg_write_file
    4.62        command
    4.63        (arguments timeout)
    4.64 -      (Res_Reconstruct.lemma_list true)
    4.65 +      (SPR.lemma_list true)
    4.66        name
    4.67        problem
    4.68    end;
    4.69 @@ -298,7 +301,7 @@
    4.70    let
    4.71      val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
    4.72    in
    4.73 -    if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
    4.74 +    if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
    4.75      else split_lines answer
    4.76    end;
    4.77  
    4.78 @@ -310,7 +313,7 @@
    4.79  
    4.80  fun the_system prefix =
    4.81    (case get_system prefix of
    4.82 -    NONE => error ("No system like " ^ quote prefix ^ " at SystemOnTPTP")
    4.83 +    NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
    4.84    | SOME sys => sys);
    4.85  
    4.86  fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
     5.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Mar 17 18:16:31 2010 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Mar 17 19:26:05 2010 +0100
     5.3 @@ -1,11 +1,11 @@
     5.4 -(*  Title:      HOL/Tools/metis_tools.ML
     5.5 +(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
     5.6      Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
     5.7      Copyright   Cambridge University 2007
     5.8  
     5.9  HOL setup for the Metis prover.
    5.10  *)
    5.11  
    5.12 -signature METIS_TOOLS =
    5.13 +signature METIS_TACTICS =
    5.14  sig
    5.15    val trace: bool Unsynchronized.ref
    5.16    val type_lits: bool Config.T
    5.17 @@ -15,15 +15,19 @@
    5.18    val setup: theory -> theory
    5.19  end
    5.20  
    5.21 -structure MetisTools: METIS_TOOLS =
    5.22 +structure Metis_Tactics : METIS_TACTICS =
    5.23  struct
    5.24  
    5.25 +structure SFC = Sledgehammer_FOL_Clause
    5.26 +structure SHC = Sledgehammer_HOL_Clause
    5.27 +structure SPR = Sledgehammer_Proof_Reconstruct
    5.28 +
    5.29  val trace = Unsynchronized.ref false;
    5.30 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    5.31 +fun trace_msg msg = if !trace then tracing (msg ()) else ();
    5.32  
    5.33  val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
    5.34  
    5.35 -datatype mode = FO | HO | FT  (*first-order, higher-order, fully-typed*)
    5.36 +datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
    5.37  
    5.38  (* ------------------------------------------------------------------------- *)
    5.39  (* Useful Theorems                                                           *)
    5.40 @@ -63,62 +67,62 @@
    5.41  
    5.42  fun metis_lit b c args = (b, (c, args));
    5.43  
    5.44 -fun hol_type_to_fol (Res_Clause.AtomV x) = Metis.Term.Var x
    5.45 -  | hol_type_to_fol (Res_Clause.AtomF x) = Metis.Term.Fn(x,[])
    5.46 -  | hol_type_to_fol (Res_Clause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
    5.47 +fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x
    5.48 +  | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[])
    5.49 +  | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
    5.50  
    5.51  (*These two functions insert type literals before the real literals. That is the
    5.52    opposite order from TPTP linkup, but maybe OK.*)
    5.53  
    5.54  fun hol_term_to_fol_FO tm =
    5.55 -  case Res_HOL_Clause.strip_comb tm of
    5.56 -      (Res_HOL_Clause.CombConst(c,_,tys), tms) =>
    5.57 +  case SHC.strip_comb tm of
    5.58 +      (SHC.CombConst(c,_,tys), tms) =>
    5.59          let val tyargs = map hol_type_to_fol tys
    5.60              val args   = map hol_term_to_fol_FO tms
    5.61          in Metis.Term.Fn (c, tyargs @ args) end
    5.62 -    | (Res_HOL_Clause.CombVar(v,_), []) => Metis.Term.Var v
    5.63 +    | (SHC.CombVar(v,_), []) => Metis.Term.Var v
    5.64      | _ => error "hol_term_to_fol_FO";
    5.65  
    5.66 -fun hol_term_to_fol_HO (Res_HOL_Clause.CombVar (a, _)) = Metis.Term.Var a
    5.67 -  | hol_term_to_fol_HO (Res_HOL_Clause.CombConst (a, _, tylist)) =
    5.68 +fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a
    5.69 +  | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) =
    5.70        Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    5.71 -  | hol_term_to_fol_HO (Res_HOL_Clause.CombApp (tm1, tm2)) =
    5.72 +  | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) =
    5.73         Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    5.74  
    5.75  (*The fully-typed translation, to avoid type errors*)
    5.76  fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
    5.77  
    5.78 -fun hol_term_to_fol_FT (Res_HOL_Clause.CombVar(a, ty)) =
    5.79 +fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) =
    5.80        wrap_type (Metis.Term.Var a, ty)
    5.81 -  | hol_term_to_fol_FT (Res_HOL_Clause.CombConst(a, ty, _)) =
    5.82 +  | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) =
    5.83        wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
    5.84 -  | hol_term_to_fol_FT (tm as Res_HOL_Clause.CombApp(tm1,tm2)) =
    5.85 +  | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) =
    5.86         wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
    5.87 -                  Res_HOL_Clause.type_of_combterm tm);
    5.88 +                  SHC.type_of_combterm tm);
    5.89  
    5.90 -fun hol_literal_to_fol FO (Res_HOL_Clause.Literal (pol, tm)) =
    5.91 -      let val (Res_HOL_Clause.CombConst(p,_,tys), tms) = Res_HOL_Clause.strip_comb tm
    5.92 +fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) =
    5.93 +      let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm
    5.94            val tylits = if p = "equal" then [] else map hol_type_to_fol tys
    5.95            val lits = map hol_term_to_fol_FO tms
    5.96        in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
    5.97 -  | hol_literal_to_fol HO (Res_HOL_Clause.Literal (pol, tm)) =
    5.98 -     (case Res_HOL_Clause.strip_comb tm of
    5.99 -          (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
   5.100 +  | hol_literal_to_fol HO (SHC.Literal (pol, tm)) =
   5.101 +     (case SHC.strip_comb tm of
   5.102 +          (SHC.CombConst("equal",_,_), tms) =>
   5.103              metis_lit pol "=" (map hol_term_to_fol_HO tms)
   5.104          | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   5.105 -  | hol_literal_to_fol FT (Res_HOL_Clause.Literal (pol, tm)) =
   5.106 -     (case Res_HOL_Clause.strip_comb tm of
   5.107 -          (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
   5.108 +  | hol_literal_to_fol FT (SHC.Literal (pol, tm)) =
   5.109 +     (case SHC.strip_comb tm of
   5.110 +          (SHC.CombConst("equal",_,_), tms) =>
   5.111              metis_lit pol "=" (map hol_term_to_fol_FT tms)
   5.112          | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   5.113  
   5.114  fun literals_of_hol_thm thy mode t =
   5.115 -      let val (lits, types_sorts) = Res_HOL_Clause.literals_of_term thy t
   5.116 +      let val (lits, types_sorts) = SHC.literals_of_term thy t
   5.117        in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   5.118  
   5.119  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   5.120 -fun metis_of_typeLit pos (Res_Clause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
   5.121 -  | metis_of_typeLit pos (Res_Clause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
   5.122 +fun metis_of_typeLit pos (SFC.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
   5.123 +  | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
   5.124  
   5.125  fun default_sort _ (TVar _) = false
   5.126    | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
   5.127 @@ -132,9 +136,9 @@
   5.128               (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
   5.129    in
   5.130        if is_conjecture then
   5.131 -          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), Res_Clause.add_typs types_sorts)
   5.132 +          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts)
   5.133        else
   5.134 -        let val tylits = Res_Clause.add_typs
   5.135 +        let val tylits = SFC.add_typs
   5.136                             (filter (not o default_sort ctxt) types_sorts)
   5.137              val mtylits = if Config.get ctxt type_lits
   5.138                            then map (metis_of_typeLit false) tylits else []
   5.139 @@ -145,13 +149,13 @@
   5.140  
   5.141  (* ARITY CLAUSE *)
   5.142  
   5.143 -fun m_arity_cls (Res_Clause.TConsLit (c,t,args)) =
   5.144 -      metis_lit true (Res_Clause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   5.145 -  | m_arity_cls (Res_Clause.TVarLit (c,str))     =
   5.146 -      metis_lit false (Res_Clause.make_type_class c) [Metis.Term.Var str];
   5.147 +fun m_arity_cls (SFC.TConsLit (c,t,args)) =
   5.148 +      metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   5.149 +  | m_arity_cls (SFC.TVarLit (c,str))     =
   5.150 +      metis_lit false (SFC.make_type_class c) [Metis.Term.Var str];
   5.151  
   5.152  (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   5.153 -fun arity_cls (Res_Clause.ArityClause{conclLit,premLits,...}) =
   5.154 +fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) =
   5.155    (TrueI,
   5.156     Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   5.157  
   5.158 @@ -160,7 +164,7 @@
   5.159  fun m_classrel_cls subclass superclass =
   5.160    [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   5.161  
   5.162 -fun classrel_cls (Res_Clause.ClassrelClause {subclass, superclass, ...}) =
   5.163 +fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) =
   5.164    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   5.165  
   5.166  (* ------------------------------------------------------------------------- *)
   5.167 @@ -209,14 +213,14 @@
   5.168    | strip_happ args x = (x, args);
   5.169  
   5.170  fun fol_type_to_isa _ (Metis.Term.Var v) =
   5.171 -     (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
   5.172 -          SOME w => Res_Reconstruct.make_tvar w
   5.173 -        | NONE   => Res_Reconstruct.make_tvar v)
   5.174 +     (case SPR.strip_prefix SFC.tvar_prefix v of
   5.175 +          SOME w => SPR.make_tvar w
   5.176 +        | NONE   => SPR.make_tvar v)
   5.177    | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   5.178 -     (case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix x of
   5.179 -          SOME tc => Term.Type (Res_Reconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   5.180 +     (case SPR.strip_prefix SFC.tconst_prefix x of
   5.181 +          SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   5.182          | NONE    =>
   5.183 -      case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix x of
   5.184 +      case SPR.strip_prefix SFC.tfree_prefix x of
   5.185            SOME tf => mk_tfree ctxt tf
   5.186          | NONE    => error ("fol_type_to_isa: " ^ x));
   5.187  
   5.188 @@ -225,10 +229,10 @@
   5.189    let val thy = ProofContext.theory_of ctxt
   5.190        val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
   5.191        fun tm_to_tt (Metis.Term.Var v) =
   5.192 -             (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
   5.193 -                  SOME w => Type (Res_Reconstruct.make_tvar w)
   5.194 +             (case SPR.strip_prefix SFC.tvar_prefix v of
   5.195 +                  SOME w => Type (SPR.make_tvar w)
   5.196                  | NONE =>
   5.197 -              case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
   5.198 +              case SPR.strip_prefix SFC.schematic_var_prefix v of
   5.199                    SOME w => Term (mk_var (w, HOLogic.typeT))
   5.200                  | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   5.201                      (*Var from Metis with a name like _nnn; possibly a type variable*)
   5.202 @@ -245,14 +249,14 @@
   5.203        and applic_to_tt ("=",ts) =
   5.204              Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
   5.205          | applic_to_tt (a,ts) =
   5.206 -            case Res_Reconstruct.strip_prefix Res_Clause.const_prefix a of
   5.207 +            case SPR.strip_prefix SFC.const_prefix a of
   5.208                  SOME b =>
   5.209 -                  let val c = Res_Reconstruct.invert_const b
   5.210 -                      val ntypes = Res_Reconstruct.num_typargs thy c
   5.211 +                  let val c = SPR.invert_const b
   5.212 +                      val ntypes = SPR.num_typargs thy c
   5.213                        val nterms = length ts - ntypes
   5.214                        val tts = map tm_to_tt ts
   5.215                        val tys = types_of (List.take(tts,ntypes))
   5.216 -                      val ntyargs = Res_Reconstruct.num_typargs thy c
   5.217 +                      val ntyargs = SPR.num_typargs thy c
   5.218                    in if length tys = ntyargs then
   5.219                           apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   5.220                       else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
   5.221 @@ -263,14 +267,14 @@
   5.222                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   5.223                       end
   5.224                | NONE => (*Not a constant. Is it a type constructor?*)
   5.225 -            case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix a of
   5.226 +            case SPR.strip_prefix SFC.tconst_prefix a of
   5.227                  SOME b =>
   5.228 -                  Type (Term.Type (Res_Reconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
   5.229 +                  Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts)))
   5.230                | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   5.231 -            case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix a of
   5.232 +            case SPR.strip_prefix SFC.tfree_prefix a of
   5.233                  SOME b => Type (mk_tfree ctxt b)
   5.234                | NONE => (*a fixed variable? They are Skolem functions.*)
   5.235 -            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix a of
   5.236 +            case SPR.strip_prefix SFC.fixed_var_prefix a of
   5.237                  SOME b =>
   5.238                    let val opr = Term.Free(b, HOLogic.typeT)
   5.239                    in  apply_list opr (length ts) (map tm_to_tt ts)  end
   5.240 @@ -281,16 +285,16 @@
   5.241  fun fol_term_to_hol_FT ctxt fol_tm =
   5.242    let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
   5.243        fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
   5.244 -             (case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
   5.245 +             (case SPR.strip_prefix SFC.schematic_var_prefix v of
   5.246                    SOME w =>  mk_var(w, dummyT)
   5.247                  | NONE   => mk_var(v, dummyT))
   5.248          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
   5.249              Const ("op =", HOLogic.typeT)
   5.250          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   5.251 -           (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
   5.252 -                SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
   5.253 +           (case SPR.strip_prefix SFC.const_prefix x of
   5.254 +                SOME c => Const (SPR.invert_const c, dummyT)
   5.255                | NONE => (*Not a constant. Is it a fixed variable??*)
   5.256 -            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
   5.257 +            case SPR.strip_prefix SFC.fixed_var_prefix x of
   5.258                  SOME v => Free (v, fol_type_to_isa ctxt ty)
   5.259                | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
   5.260          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   5.261 @@ -301,10 +305,10 @@
   5.262          | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   5.263              list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
   5.264          | cvt (t as Metis.Term.Fn (x, [])) =
   5.265 -           (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
   5.266 -                SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
   5.267 +           (case SPR.strip_prefix SFC.const_prefix x of
   5.268 +                SOME c => Const (SPR.invert_const c, dummyT)
   5.269                | NONE => (*Not a constant. Is it a fixed variable??*)
   5.270 -            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
   5.271 +            case SPR.strip_prefix SFC.fixed_var_prefix x of
   5.272                  SOME v => Free (v, dummyT)
   5.273                | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
   5.274                    fol_term_to_hol_RAW ctxt t))
   5.275 @@ -383,9 +387,9 @@
   5.276                                         " in " ^ Display.string_of_thm ctxt i_th);
   5.277                   NONE)
   5.278        fun remove_typeinst (a, t) =
   5.279 -            case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix a of
   5.280 +            case SPR.strip_prefix SFC.schematic_var_prefix a of
   5.281                  SOME b => SOME (b, t)
   5.282 -              | NONE   => case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix a of
   5.283 +              | NONE   => case SPR.strip_prefix SFC.tvar_prefix a of
   5.284                  SOME _ => NONE          (*type instantiations are forbidden!*)
   5.285                | NONE   => SOME (a,t)    (*internal Metis var?*)
   5.286        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   5.287 @@ -452,7 +456,7 @@
   5.288    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   5.289  
   5.290  fun get_ty_arg_size _ (Const ("op =", _)) = 0  (*equality has no type arguments*)
   5.291 -  | get_ty_arg_size thy (Const (c, _)) = (Res_Reconstruct.num_typargs thy c handle TYPE _ => 0)
   5.292 +  | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0)
   5.293    | get_ty_arg_size _ _ = 0;
   5.294  
   5.295  (* INFERENCE RULE: EQUALITY *)
   5.296 @@ -538,7 +542,7 @@
   5.297    | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
   5.298        equality_inf ctxt mode f_lit f_p f_r;
   5.299  
   5.300 -fun real_literal (_, (c, _)) = not (String.isPrefix Res_Clause.class_prefix c);
   5.301 +fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c);
   5.302  
   5.303  fun translate _ _ thpairs [] = thpairs
   5.304    | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   5.305 @@ -564,23 +568,23 @@
   5.306  (* Translation of HO Clauses                                                 *)
   5.307  (* ------------------------------------------------------------------------- *)
   5.308  
   5.309 -fun cnf_th thy th = hd (Res_Axioms.cnf_axiom thy th);
   5.310 +fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th);
   5.311  
   5.312  val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
   5.313  val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
   5.314  
   5.315 -val comb_I = cnf_th @{theory} Res_HOL_Clause.comb_I;
   5.316 -val comb_K = cnf_th @{theory} Res_HOL_Clause.comb_K;
   5.317 -val comb_B = cnf_th @{theory} Res_HOL_Clause.comb_B;
   5.318 -val comb_C = cnf_th @{theory} Res_HOL_Clause.comb_C;
   5.319 -val comb_S = cnf_th @{theory} Res_HOL_Clause.comb_S;
   5.320 +val comb_I = cnf_th @{theory} SHC.comb_I;
   5.321 +val comb_K = cnf_th @{theory} SHC.comb_K;
   5.322 +val comb_B = cnf_th @{theory} SHC.comb_B;
   5.323 +val comb_C = cnf_th @{theory} SHC.comb_C;
   5.324 +val comb_S = cnf_th @{theory} SHC.comb_S;
   5.325  
   5.326  fun type_ext thy tms =
   5.327 -  let val subs = Res_ATP.tfree_classes_of_terms tms
   5.328 -      val supers = Res_ATP.tvar_classes_of_terms tms
   5.329 -      and tycons = Res_ATP.type_consts_of_terms thy tms
   5.330 -      val (supers', arity_clauses) = Res_Clause.make_arity_clauses thy tycons supers
   5.331 -      val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
   5.332 +  let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms
   5.333 +      val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms
   5.334 +      and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms
   5.335 +      val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers
   5.336 +      val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
   5.337    in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   5.338    end;
   5.339  
   5.340 @@ -590,7 +594,7 @@
   5.341  
   5.342  type logic_map =
   5.343    {axioms : (Metis.Thm.thm * thm) list,
   5.344 -   tfrees : Res_Clause.type_literal list};
   5.345 +   tfrees : SFC.type_literal list};
   5.346  
   5.347  fun const_in_metis c (pred, tm_list) =
   5.348    let
   5.349 @@ -602,7 +606,7 @@
   5.350  (*Extract TFree constraints from context to include as conjecture clauses*)
   5.351  fun init_tfrees ctxt =
   5.352    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
   5.353 -  in  Res_Clause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
   5.354 +  in  SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
   5.355  
   5.356  (*transform isabelle type / arity clause to metis clause *)
   5.357  fun add_type_thm [] lmap = lmap
   5.358 @@ -663,7 +667,8 @@
   5.359  (* Main function to start metis prove and reconstruction *)
   5.360  fun FOL_SOLVE mode ctxt cls ths0 =
   5.361    let val thy = ProofContext.theory_of ctxt
   5.362 -      val th_cls_pairs = map (fn th => (Thm.get_name_hint th, Res_Axioms.cnf_axiom thy th)) ths0
   5.363 +      val th_cls_pairs =
   5.364 +        map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0
   5.365        val ths = maps #2 th_cls_pairs
   5.366        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   5.367        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   5.368 @@ -672,7 +677,7 @@
   5.369        val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
   5.370        val _ = if null tfrees then ()
   5.371                else (trace_msg (fn () => "TFREE CLAUSES");
   5.372 -                    app (fn tf => trace_msg (fn _ => Res_Clause.tptp_of_typeLit true tf)) tfrees)
   5.373 +                    app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees)
   5.374        val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   5.375        val thms = map #1 axioms
   5.376        val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   5.377 @@ -714,12 +719,12 @@
   5.378    let val _ = trace_msg (fn () =>
   5.379          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   5.380    in
   5.381 -    if exists_type Res_Axioms.type_has_topsort (prop_of st0)
   5.382 +    if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0)
   5.383      then raise METIS "Metis: Proof state contains the universal sort {}"
   5.384      else
   5.385 -      (Meson.MESON Res_Axioms.neg_clausify
   5.386 +      (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify
   5.387          (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
   5.388 -          THEN Res_Axioms.expand_defs_tac st0) st0
   5.389 +          THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0
   5.390    end
   5.391    handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
   5.392  
   5.393 @@ -736,7 +741,7 @@
   5.394    method @{binding metisF} FO "METIS for FOL problems" #>
   5.395    method @{binding metisFT} FT "METIS with fully-typed translation" #>
   5.396    Method.setup @{binding finish_clausify}
   5.397 -    (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
   5.398 +    (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl))))
   5.399      "cleanup after conversion to clauses";
   5.400  
   5.401  end;
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Mar 17 18:16:31 2010 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Mar 17 19:26:05 2010 +0100
     6.3 @@ -1,9 +1,14 @@
     6.4 -(*  Title:      HOL/Tools/res_atp.ML
     6.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     6.6      Author:     Jia Meng, Cambridge University Computer Laboratory, NICTA
     6.7  *)
     6.8  
     6.9 -signature RES_ATP =
    6.10 +signature SLEDGEHAMMER_FACT_FILTER =
    6.11  sig
    6.12 +  type classrelClause = Sledgehammer_FOL_Clause.classrelClause
    6.13 +  type arityClause = Sledgehammer_FOL_Clause.arityClause
    6.14 +  type axiom_name = Sledgehammer_HOL_Clause.axiom_name
    6.15 +  type clause = Sledgehammer_HOL_Clause.clause
    6.16 +  type clause_id = Sledgehammer_HOL_Clause.clause_id
    6.17    datatype mode = Auto | Fol | Hol
    6.18    val tvar_classes_of_terms : term list -> string list
    6.19    val tfree_classes_of_terms : term list -> string list
    6.20 @@ -11,16 +16,25 @@
    6.21    val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
    6.22      (thm * (string * int)) list
    6.23    val prepare_clauses : bool -> thm list -> thm list ->
    6.24 -    (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list ->
    6.25 -    (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list -> theory ->
    6.26 -    Res_HOL_Clause.axiom_name vector *
    6.27 -      (Res_HOL_Clause.clause list * Res_HOL_Clause.clause list * Res_HOL_Clause.clause list *
    6.28 -      Res_HOL_Clause.clause list * Res_Clause.classrelClause list * Res_Clause.arityClause list)
    6.29 +    (thm * (axiom_name * clause_id)) list ->
    6.30 +    (thm * (axiom_name * clause_id)) list -> theory ->
    6.31 +    axiom_name vector *
    6.32 +      (clause list * clause list * clause list *
    6.33 +      clause list * classrelClause list * arityClause list)
    6.34  end;
    6.35  
    6.36 -structure Res_ATP: RES_ATP =
    6.37 +structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    6.38  struct
    6.39  
    6.40 +structure SFC = Sledgehammer_FOL_Clause
    6.41 +structure SFP = Sledgehammer_Fact_Preprocessor
    6.42 +structure SHC = Sledgehammer_HOL_Clause
    6.43 +
    6.44 +type classrelClause = SFC.classrelClause
    6.45 +type arityClause = SFC.arityClause
    6.46 +type axiom_name = SHC.axiom_name
    6.47 +type clause = SHC.clause
    6.48 +type clause_id = SHC.clause_id
    6.49  
    6.50  (********************************************************************)
    6.51  (* some settings for both background automatic ATP calling procedure*)
    6.52 @@ -238,10 +252,10 @@
    6.53        let val cls = sort compare_pairs newpairs
    6.54            val accepted = List.take (cls, max_new)
    6.55        in
    6.56 -        Res_Axioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
    6.57 +        SFP.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
    6.58                         ", exceeds the limit of " ^ Int.toString (max_new)));
    6.59 -        Res_Axioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    6.60 -        Res_Axioms.trace_msg (fn () => "Actually passed: " ^
    6.61 +        SFP.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    6.62 +        SFP.trace_msg (fn () => "Actually passed: " ^
    6.63            space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
    6.64  
    6.65          (map #1 accepted, map #1 (List.drop (cls, max_new)))
    6.66 @@ -256,7 +270,7 @@
    6.67                  val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
    6.68                  val newp = p + (1.0-p) / convergence
    6.69              in
    6.70 -              Res_Axioms.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
    6.71 +              SFP.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
    6.72                 (map #1 newrels) @ 
    6.73                 (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
    6.74              end
    6.75 @@ -264,12 +278,12 @@
    6.76              let val weight = clause_weight ctab rel_consts consts_typs
    6.77              in
    6.78                if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
    6.79 -              then (Res_Axioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
    6.80 +              then (SFP.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
    6.81                                              " passes: " ^ Real.toString weight));
    6.82                      relevant ((ax,weight)::newrels, rejects) axs)
    6.83                else relevant (newrels, ax::rejects) axs
    6.84              end
    6.85 -    in  Res_Axioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
    6.86 +    in  SFP.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
    6.87          relevant ([],[]) 
    6.88      end;
    6.89          
    6.90 @@ -278,12 +292,12 @@
    6.91   then
    6.92    let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
    6.93        val goal_const_tab = get_goal_consts_typs thy goals
    6.94 -      val _ = Res_Axioms.trace_msg (fn () => ("Initial constants: " ^
    6.95 +      val _ = SFP.trace_msg (fn () => ("Initial constants: " ^
    6.96                                   space_implode ", " (Symtab.keys goal_const_tab)));
    6.97        val rels = relevant_clauses max_new thy const_tab (pass_mark) 
    6.98                     goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
    6.99    in
   6.100 -      Res_Axioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   6.101 +      SFP.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   6.102        rels
   6.103    end
   6.104   else axioms;
   6.105 @@ -337,7 +351,7 @@
   6.106  fun make_unique xs =
   6.107    let val ht = mk_clause_table 7000
   6.108    in
   6.109 -      Res_Axioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
   6.110 +      SFP.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
   6.111        app (ignore o Polyhash.peekInsert ht) xs;
   6.112        Polyhash.listItems ht
   6.113    end;
   6.114 @@ -369,7 +383,7 @@
   6.115  
   6.116            val name1 = Facts.extern facts name;
   6.117            val name2 = Name_Space.extern full_space name;
   6.118 -          val ths = filter_out Res_Axioms.bad_for_atp ths0;
   6.119 +          val ths = filter_out SFP.bad_for_atp ths0;
   6.120          in
   6.121            if Facts.is_concealed facts name orelse null ths orelse
   6.122              run_blacklist_filter andalso is_package_def name then I
   6.123 @@ -389,7 +403,7 @@
   6.124  
   6.125  (*Ignore blacklisted basenames*)
   6.126  fun add_multi_names (a, ths) pairs =
   6.127 -  if (Long_Name.base_name a) mem_string Res_Axioms.multi_base_blacklist then pairs
   6.128 +  if (Long_Name.base_name a) mem_string SFP.multi_base_blacklist then pairs
   6.129    else add_single_names (a, ths) pairs;
   6.130  
   6.131  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   6.132 @@ -411,7 +425,7 @@
   6.133  
   6.134  fun get_all_lemmas ctxt =
   6.135    let val included_thms =
   6.136 -        tap (fn ths => Res_Axioms.trace_msg
   6.137 +        tap (fn ths => SFP.trace_msg
   6.138                       (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   6.139              (name_thm_pairs ctxt)
   6.140    in
   6.141 @@ -519,7 +533,7 @@
   6.142      val thy = ProofContext.theory_of ctxt
   6.143      val isFO = isFO thy goal_cls
   6.144      val included_cls = get_all_lemmas ctxt
   6.145 -      |> Res_Axioms.cnf_rules_pairs thy |> make_unique
   6.146 +      |> SFP.cnf_rules_pairs thy |> make_unique
   6.147        |> restrict_to_logic thy isFO
   6.148        |> remove_unwanted_clauses
   6.149    in
   6.150 @@ -532,24 +546,24 @@
   6.151    let
   6.152      (* add chain thms *)
   6.153      val chain_cls =
   6.154 -      Res_Axioms.cnf_rules_pairs thy (filter check_named (map Res_Axioms.pairname chain_ths))
   6.155 +      SFP.cnf_rules_pairs thy (filter check_named (map SFP.pairname chain_ths))
   6.156      val axcls = chain_cls @ axcls
   6.157      val extra_cls = chain_cls @ extra_cls
   6.158      val isFO = isFO thy goal_cls
   6.159      val ccls = subtract_cls goal_cls extra_cls
   6.160 -    val _ = app (fn th => Res_Axioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   6.161 +    val _ = app (fn th => SFP.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   6.162      val ccltms = map prop_of ccls
   6.163      and axtms = map (prop_of o #1) extra_cls
   6.164      val subs = tfree_classes_of_terms ccltms
   6.165      and supers = tvar_classes_of_terms axtms
   6.166      and tycons = type_consts_of_terms thy (ccltms@axtms)
   6.167      (*TFrees in conjecture clauses; TVars in axiom clauses*)
   6.168 -    val conjectures = Res_HOL_Clause.make_conjecture_clauses dfg thy ccls
   6.169 -    val (_, extra_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy extra_cls)
   6.170 -    val (clnames,axiom_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy axcls)
   6.171 -    val helper_clauses = Res_HOL_Clause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
   6.172 -    val (supers',arity_clauses) = Res_Clause.make_arity_clauses_dfg dfg thy tycons supers
   6.173 -    val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
   6.174 +    val conjectures = SHC.make_conjecture_clauses dfg thy ccls
   6.175 +    val (_, extra_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy extra_cls)
   6.176 +    val (clnames,axiom_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy axcls)
   6.177 +    val helper_clauses = SHC.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
   6.178 +    val (supers',arity_clauses) = SFC.make_arity_clauses_dfg dfg thy tycons supers
   6.179 +    val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
   6.180    in
   6.181      (Vector.fromList clnames,
   6.182        (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Mar 17 18:16:31 2010 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Mar 17 19:26:05 2010 +0100
     7.3 @@ -1,10 +1,10 @@
     7.4 -(*  Title:      HOL/Tools/res_axioms.ML
     7.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
     7.6      Author:     Jia Meng, Cambridge University Computer Laboratory
     7.7  
     7.8  Transformation of axiom rules (elim/intro/etc) into CNF forms.
     7.9  *)
    7.10  
    7.11 -signature RES_AXIOMS =
    7.12 +signature SLEDGEHAMMER_FACT_PREPROCESSOR =
    7.13  sig
    7.14    val trace: bool Unsynchronized.ref
    7.15    val trace_msg: (unit -> string) -> unit
    7.16 @@ -23,7 +23,7 @@
    7.17    val setup: theory -> theory
    7.18  end;
    7.19  
    7.20 -structure Res_Axioms: RES_AXIOMS =
    7.21 +structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR =
    7.22  struct
    7.23  
    7.24  val trace = Unsynchronized.ref false;
    7.25 @@ -285,7 +285,7 @@
    7.26    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
    7.27  
    7.28  
    7.29 -(*** Blacklisting (duplicated in Res_ATP?) ***)
    7.30 +(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***)
    7.31  
    7.32  val max_lambda_nesting = 3;
    7.33  
    7.34 @@ -385,14 +385,16 @@
    7.35  fun cnf_rules_pairs_aux _ pairs [] = pairs
    7.36    | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
    7.37        let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
    7.38 -                       handle THM _ => pairs | Res_Clause.CLAUSE _ => pairs
    7.39 +                       handle THM _ => pairs |
    7.40 +                              Sledgehammer_FOL_Clause.CLAUSE _ => pairs
    7.41        in  cnf_rules_pairs_aux thy pairs' ths  end;
    7.42  
    7.43  (*The combination of rev and tail recursion preserves the original order*)
    7.44  fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
    7.45  
    7.46  
    7.47 -(**** Convert all facts of the theory into clauses (Res_Clause.clause, or Res_HOL_Clause.clause) ****)
    7.48 +(**** Convert all facts of the theory into clauses
    7.49 +      (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****)
    7.50  
    7.51  local
    7.52  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Mar 17 18:16:31 2010 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Mar 17 19:26:05 2010 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Tools/res_clause.ML
     8.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
     8.6      Author:     Jia Meng, Cambridge University Computer Laboratory
     8.7  
     8.8  Storing/printing FOL clauses and arity clauses.  Typed equality is
     8.9 @@ -7,7 +7,7 @@
    8.10  FIXME: combine with res_hol_clause!
    8.11  *)
    8.12  
    8.13 -signature RES_CLAUSE =
    8.14 +signature SLEDGEHAMMER_FOL_CLAUSE =
    8.15  sig
    8.16    val schematic_var_prefix: string
    8.17    val fixed_var_prefix: string
    8.18 @@ -77,7 +77,7 @@
    8.19    val tptp_classrelClause : classrelClause -> string
    8.20  end
    8.21  
    8.22 -structure Res_Clause: RES_CLAUSE =
    8.23 +structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
    8.24  struct
    8.25  
    8.26  val schematic_var_prefix = "V_";
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Mar 17 18:16:31 2010 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Mar 17 19:26:05 2010 +0100
     9.3 @@ -1,10 +1,10 @@
     9.4 -(*  Title:      HOL/Tools/res_hol_clause.ML
     9.5 +(*  Title:      HOL/Sledgehammer/sledgehammer_hol_clause.ML
     9.6      Author:     Jia Meng, NICTA
     9.7  
     9.8  FOL clauses translated from HOL formulae.
     9.9  *)
    9.10  
    9.11 -signature RES_HOL_CLAUSE =
    9.12 +signature SLEDGEHAMMER_HOL_CLAUSE =
    9.13  sig
    9.14    val ext: thm
    9.15    val comb_I: thm
    9.16 @@ -17,13 +17,13 @@
    9.17    type polarity = bool
    9.18    type clause_id = int
    9.19    datatype combterm =
    9.20 -      CombConst of string * Res_Clause.fol_type * Res_Clause.fol_type list (*Const and Free*)
    9.21 -    | CombVar of string * Res_Clause.fol_type
    9.22 +      CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*)
    9.23 +    | CombVar of string * Sledgehammer_FOL_Clause.fol_type
    9.24      | CombApp of combterm * combterm
    9.25    datatype literal = Literal of polarity * combterm
    9.26    datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
    9.27 -                    kind: Res_Clause.kind,literals: literal list, ctypes_sorts: typ list}
    9.28 -  val type_of_combterm: combterm -> Res_Clause.fol_type
    9.29 +                    kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list}
    9.30 +  val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type
    9.31    val strip_comb: combterm -> combterm * combterm list
    9.32    val literals_of_term: theory -> term -> literal list * typ list
    9.33    exception TOO_TRIVIAL
    9.34 @@ -38,18 +38,18 @@
    9.35         clause list
    9.36    val tptp_write_file: bool -> Path.T ->
    9.37      clause list * clause list * clause list * clause list *
    9.38 -    Res_Clause.classrelClause list * Res_Clause.arityClause list ->
    9.39 +    Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
    9.40      int * int
    9.41    val dfg_write_file: bool -> Path.T ->
    9.42      clause list * clause list * clause list * clause list *
    9.43 -    Res_Clause.classrelClause list * Res_Clause.arityClause list ->
    9.44 +    Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list ->
    9.45      int * int
    9.46  end
    9.47  
    9.48 -structure Res_HOL_Clause: RES_HOL_CLAUSE =
    9.49 +structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    9.50  struct
    9.51  
    9.52 -structure RC = Res_Clause;   (* FIXME avoid structure alias *)
    9.53 +structure SFC = Sledgehammer_FOL_Clause;
    9.54  
    9.55  (* theorems for combinators and function extensionality *)
    9.56  val ext = thm "HOL.ext";
    9.57 @@ -86,8 +86,8 @@
    9.58  type polarity = bool;
    9.59  type clause_id = int;
    9.60  
    9.61 -datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
    9.62 -                  | CombVar of string * RC.fol_type
    9.63 +datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*)
    9.64 +                  | CombVar of string * SFC.fol_type
    9.65                    | CombApp of combterm * combterm
    9.66  
    9.67  datatype literal = Literal of polarity * combterm;
    9.68 @@ -96,7 +96,7 @@
    9.69           Clause of {clause_id: clause_id,
    9.70                      axiom_name: axiom_name,
    9.71                      th: thm,
    9.72 -                    kind: RC.kind,
    9.73 +                    kind: SFC.kind,
    9.74                      literals: literal list,
    9.75                      ctypes_sorts: typ list};
    9.76  
    9.77 @@ -119,20 +119,20 @@
    9.78  
    9.79  fun type_of dfg (Type (a, Ts)) =
    9.80        let val (folTypes,ts) = types_of dfg Ts
    9.81 -      in  (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts)  end
    9.82 +      in  (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts)  end
    9.83    | type_of _ (tp as TFree (a, _)) =
    9.84 -      (RC.AtomF (RC.make_fixed_type_var a), [tp])
    9.85 +      (SFC.AtomF (SFC.make_fixed_type_var a), [tp])
    9.86    | type_of _ (tp as TVar (v, _)) =
    9.87 -      (RC.AtomV (RC.make_schematic_type_var v), [tp])
    9.88 +      (SFC.AtomV (SFC.make_schematic_type_var v), [tp])
    9.89  and types_of dfg Ts =
    9.90        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    9.91 -      in  (folTyps, RC.union_all ts)  end;
    9.92 +      in  (folTyps, SFC.union_all ts)  end;
    9.93  
    9.94  (* same as above, but no gathering of sort information *)
    9.95  fun simp_type_of dfg (Type (a, Ts)) =
    9.96 -      RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    9.97 -  | simp_type_of _ (TFree (a, _)) = RC.AtomF(RC.make_fixed_type_var a)
    9.98 -  | simp_type_of _ (TVar (v, _)) = RC.AtomV(RC.make_schematic_type_var v);
    9.99 +      SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
   9.100 +  | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a)
   9.101 +  | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v);
   9.102  
   9.103  
   9.104  fun const_type_of dfg thy (c,t) =
   9.105 @@ -142,21 +142,21 @@
   9.106  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   9.107  fun combterm_of dfg thy (Const(c,t)) =
   9.108        let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
   9.109 -          val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list)
   9.110 +          val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list)
   9.111        in  (c',ts)  end
   9.112    | combterm_of dfg _ (Free(v,t)) =
   9.113        let val (tp,ts) = type_of dfg t
   9.114 -          val v' = CombConst(RC.make_fixed_var v, tp, [])
   9.115 +          val v' = CombConst(SFC.make_fixed_var v, tp, [])
   9.116        in  (v',ts)  end
   9.117    | combterm_of dfg _ (Var(v,t)) =
   9.118        let val (tp,ts) = type_of dfg t
   9.119 -          val v' = CombVar(RC.make_schematic_var v,tp)
   9.120 +          val v' = CombVar(SFC.make_schematic_var v,tp)
   9.121        in  (v',ts)  end
   9.122    | combterm_of dfg thy (P $ Q) =
   9.123        let val (P',tsP) = combterm_of dfg thy P
   9.124            val (Q',tsQ) = combterm_of dfg thy Q
   9.125        in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
   9.126 -  | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
   9.127 +  | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t);
   9.128  
   9.129  fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
   9.130    | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
   9.131 @@ -189,7 +189,7 @@
   9.132  
   9.133  
   9.134  fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
   9.135 -  let val cls = make_clause dfg thy (id, name, RC.Axiom, th)
   9.136 +  let val cls = make_clause dfg thy (id, name, SFC.Axiom, th)
   9.137    in
   9.138        if isTaut cls then pairs else (name,cls)::pairs
   9.139    end;
   9.140 @@ -198,7 +198,7 @@
   9.141  
   9.142  fun make_conjecture_clauses_aux _ _ _ [] = []
   9.143    | make_conjecture_clauses_aux dfg thy n (th::ths) =
   9.144 -      make_clause dfg thy (n,"conjecture", RC.Conjecture, th) ::
   9.145 +      make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) ::
   9.146        make_conjecture_clauses_aux dfg thy (n+1) ths;
   9.147  
   9.148  fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
   9.149 @@ -211,7 +211,7 @@
   9.150  (**********************************************************************)
   9.151  
   9.152  (*Result of a function type; no need to check that the argument type matches.*)
   9.153 -fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
   9.154 +fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2
   9.155    | result_type _ = error "result_type"
   9.156  
   9.157  fun type_of_combterm (CombConst (_, tp, _)) = tp
   9.158 @@ -231,10 +231,10 @@
   9.159  
   9.160  fun wrap_type t_full (s, tp) =
   9.161    if t_full then
   9.162 -      type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
   9.163 +      type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp]
   9.164    else s;
   9.165  
   9.166 -fun apply ss = "hAPP" ^ RC.paren_pack ss;
   9.167 +fun apply ss = "hAPP" ^ SFC.paren_pack ss;
   9.168  
   9.169  fun rev_apply (v, []) = v
   9.170    | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
   9.171 @@ -251,10 +251,10 @@
   9.172                                           Int.toString nargs ^ " but is applied to " ^
   9.173                                           space_implode ", " args)
   9.174            val args2 = List.drop(args, nargs)
   9.175 -          val targs = if not t_full then map RC.string_of_fol_type tvars
   9.176 +          val targs = if not t_full then map SFC.string_of_fol_type tvars
   9.177                        else []
   9.178        in
   9.179 -          string_apply (c ^ RC.paren_pack (args1@targs), args2)
   9.180 +          string_apply (c ^ SFC.paren_pack (args1@targs), args2)
   9.181        end
   9.182    | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
   9.183    | string_of_applic _ _ _ = error "string_of_applic";
   9.184 @@ -271,13 +271,13 @@
   9.185  
   9.186  (*Boolean-valued terms are here converted to literals.*)
   9.187  fun boolify params t =
   9.188 -  "hBOOL" ^ RC.paren_pack [string_of_combterm params t];
   9.189 +  "hBOOL" ^ SFC.paren_pack [string_of_combterm params t];
   9.190  
   9.191  fun string_of_predicate (params as (_,_,cnh)) t =
   9.192    case t of
   9.193        (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   9.194            (*DFG only: new TPTP prefers infix equality*)
   9.195 -          ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
   9.196 +          ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
   9.197      | _ =>
   9.198            case #1 (strip_comb t) of
   9.199                CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
   9.200 @@ -293,28 +293,28 @@
   9.201  fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
   9.202        tptp_of_equality params pol (t1,t2)
   9.203    | tptp_literal params (Literal(pol,pred)) =
   9.204 -      RC.tptp_sign pol (string_of_predicate params pred);
   9.205 +      SFC.tptp_sign pol (string_of_predicate params pred);
   9.206  
   9.207  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   9.208    the latter should only occur in conjecture clauses.*)
   9.209  fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
   9.210        (map (tptp_literal params) literals, 
   9.211 -       map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
   9.212 +       map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts));
   9.213  
   9.214  fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) =
   9.215 -  let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls
   9.216 +  let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls
   9.217    in
   9.218 -      (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   9.219 +      (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   9.220    end;
   9.221  
   9.222  
   9.223  (*** dfg format ***)
   9.224  
   9.225 -fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred);
   9.226 +fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred);
   9.227  
   9.228  fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
   9.229        (map (dfg_literal params) literals, 
   9.230 -       map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
   9.231 +       map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts));
   9.232  
   9.233  fun get_uvars (CombConst _) vars = vars
   9.234    | get_uvars (CombVar(v,_)) vars = (v::vars)
   9.235 @@ -322,20 +322,20 @@
   9.236  
   9.237  fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   9.238  
   9.239 -fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
   9.240 +fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals);
   9.241  
   9.242  fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   9.243 -  let val (lits,tylits) = dfg_type_lits params (kind = RC.Conjecture) cls
   9.244 +  let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls
   9.245        val vars = dfg_vars cls
   9.246 -      val tvars = RC.get_tvar_strs ctypes_sorts
   9.247 +      val tvars = SFC.get_tvar_strs ctypes_sorts
   9.248    in
   9.249 -      (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
   9.250 +      (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits)
   9.251    end;
   9.252  
   9.253  
   9.254  (** For DFG format: accumulate function and predicate declarations **)
   9.255  
   9.256 -fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
   9.257 +fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars;
   9.258  
   9.259  fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
   9.260        if c = "equal" then (addtypes tvars funcs, preds)
   9.261 @@ -348,7 +348,7 @@
   9.262              else (addtypes tvars funcs, addit preds)
   9.263          end
   9.264    | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
   9.265 -      (RC.add_foltype_funcs (ctp,funcs), preds)
   9.266 +      (SFC.add_foltype_funcs (ctp,funcs), preds)
   9.267    | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
   9.268  
   9.269  fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
   9.270 @@ -358,23 +358,23 @@
   9.271      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   9.272  
   9.273  fun decls_of_clauses params clauses arity_clauses =
   9.274 -  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
   9.275 +  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab)
   9.276        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   9.277        val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
   9.278    in
   9.279 -      (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
   9.280 +      (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses),
   9.281         Symtab.dest predtab)
   9.282    end;
   9.283  
   9.284  fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   9.285 -  List.foldl RC.add_type_sort_preds preds ctypes_sorts
   9.286 +  List.foldl SFC.add_type_sort_preds preds ctypes_sorts
   9.287    handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
   9.288  
   9.289  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   9.290  fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   9.291      Symtab.dest
   9.292 -        (List.foldl RC.add_classrelClause_preds
   9.293 -               (List.foldl RC.add_arityClause_preds
   9.294 +        (List.foldl SFC.add_classrelClause_preds
   9.295 +               (List.foldl SFC.add_arityClause_preds
   9.296                        (List.foldl add_clause_preds Symtab.empty clauses)
   9.297                        arity_clauses)
   9.298                 clsrel_clauses)
   9.299 @@ -404,7 +404,8 @@
   9.300    else ct;
   9.301  
   9.302  fun cnf_helper_thms thy =
   9.303 -  Res_Axioms.cnf_rules_pairs thy o map Res_Axioms.pairname
   9.304 +  Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy
   9.305 +  o map Sledgehammer_Fact_Preprocessor.pairname
   9.306  
   9.307  fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   9.308    if isFO then []  (*first-order*)
   9.309 @@ -454,7 +455,8 @@
   9.310    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   9.311  
   9.312  fun display_arity const_needs_hBOOL (c,n) =
   9.313 -  Res_Axioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
   9.314 +  Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^
   9.315 +                " arity:\t" ^ Int.toString n ^
   9.316                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
   9.317  
   9.318  fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
   9.319 @@ -476,14 +478,14 @@
   9.320      val (cma, cnh) = count_constants clauses
   9.321      val params = (t_full, cma, cnh)
   9.322      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   9.323 -    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   9.324 +    val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
   9.325      val _ =
   9.326        File.write_list file (
   9.327          map (#1 o (clause2tptp params)) axclauses @
   9.328          tfree_clss @
   9.329          tptp_clss @
   9.330 -        map RC.tptp_classrelClause classrel_clauses @
   9.331 -        map RC.tptp_arity_clause arity_clauses @
   9.332 +        map SFC.tptp_classrelClause classrel_clauses @
   9.333 +        map SFC.tptp_arity_clause arity_clauses @
   9.334          map (#1 o (clause2tptp params)) helper_clauses)
   9.335      in (length axclauses + 1, length tfree_clss + length tptp_clss)
   9.336    end;
   9.337 @@ -500,20 +502,20 @@
   9.338      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
   9.339      and probname = Path.implode (Path.base file)
   9.340      val axstrs = map (#1 o (clause2dfg params)) axclauses
   9.341 -    val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   9.342 +    val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss)
   9.343      val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
   9.344      val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   9.345      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   9.346      val _ =
   9.347        File.write_list file (
   9.348 -        RC.string_of_start probname ::
   9.349 -        RC.string_of_descrip probname ::
   9.350 -        RC.string_of_symbols (RC.string_of_funcs funcs)
   9.351 -          (RC.string_of_preds (cl_preds @ ty_preds)) ::
   9.352 +        SFC.string_of_start probname ::
   9.353 +        SFC.string_of_descrip probname ::
   9.354 +        SFC.string_of_symbols (SFC.string_of_funcs funcs)
   9.355 +          (SFC.string_of_preds (cl_preds @ ty_preds)) ::
   9.356          "list_of_clauses(axioms,cnf).\n" ::
   9.357          axstrs @
   9.358 -        map RC.dfg_classrelClause classrel_clauses @
   9.359 -        map RC.dfg_arity_clause arity_clauses @
   9.360 +        map SFC.dfg_classrelClause classrel_clauses @
   9.361 +        map SFC.dfg_arity_clause arity_clauses @
   9.362          helper_clauses_strs @
   9.363          ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @
   9.364          tfree_clss @
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Mar 17 18:16:31 2010 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Mar 17 19:26:05 2010 +0100
    10.3 @@ -1,10 +1,10 @@
    10.4 -(*  Title:      HOL/Tools/res_reconstruct.ML
    10.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
    10.6      Author:     Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory
    10.7  
    10.8  Transfer of proofs from external provers.
    10.9  *)
   10.10  
   10.11 -signature RES_RECONSTRUCT =
   10.12 +signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
   10.13  sig
   10.14    val chained_hint: string
   10.15  
   10.16 @@ -24,13 +24,15 @@
   10.17      string * string vector * (int * int) * Proof.context * thm * int -> string * string list
   10.18  end;
   10.19  
   10.20 -structure Res_Reconstruct : RES_RECONSTRUCT =
   10.21 +structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
   10.22  struct
   10.23  
   10.24 +structure SFC = Sledgehammer_FOL_Clause
   10.25 +
   10.26  val trace_path = Path.basic "atp_trace";
   10.27  
   10.28  fun trace s =
   10.29 -  if ! Res_Axioms.trace then File.append (File.tmp_path trace_path) s
   10.30 +  if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s
   10.31    else ();
   10.32  
   10.33  fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
   10.34 @@ -107,12 +109,12 @@
   10.35  (*If string s has the prefix s1, return the result of deleting it.*)
   10.36  fun strip_prefix s1 s =
   10.37    if String.isPrefix s1 s
   10.38 -  then SOME (Res_Clause.undo_ascii_of (String.extract (s, size s1, NONE)))
   10.39 +  then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE)))
   10.40    else NONE;
   10.41  
   10.42  (*Invert the table of translations between Isabelle and ATPs*)
   10.43  val type_const_trans_table_inv =
   10.44 -      Symtab.make (map swap (Symtab.dest Res_Clause.type_const_trans_table));
   10.45 +      Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table));
   10.46  
   10.47  fun invert_type_const c =
   10.48      case Symtab.lookup type_const_trans_table_inv c of
   10.49 @@ -130,15 +132,15 @@
   10.50      | Br (a,ts) =>
   10.51          let val Ts = map type_of_stree ts
   10.52          in
   10.53 -          case strip_prefix Res_Clause.tconst_prefix a of
   10.54 +          case strip_prefix SFC.tconst_prefix a of
   10.55                SOME b => Type(invert_type_const b, Ts)
   10.56              | NONE =>
   10.57                  if not (null ts) then raise STREE t  (*only tconsts have type arguments*)
   10.58                  else
   10.59 -                case strip_prefix Res_Clause.tfree_prefix a of
   10.60 +                case strip_prefix SFC.tfree_prefix a of
   10.61                      SOME b => TFree("'" ^ b, HOLogic.typeS)
   10.62                    | NONE =>
   10.63 -                case strip_prefix Res_Clause.tvar_prefix a of
   10.64 +                case strip_prefix SFC.tvar_prefix a of
   10.65                      SOME b => make_tvar b
   10.66                    | NONE => make_tvar a   (*Variable from the ATP, say X1*)
   10.67          end;
   10.68 @@ -146,7 +148,7 @@
   10.69  (*Invert the table of translations between Isabelle and ATPs*)
   10.70  val const_trans_table_inv =
   10.71        Symtab.update ("fequal", "op =")
   10.72 -        (Symtab.make (map swap (Symtab.dest Res_Clause.const_trans_table)));
   10.73 +        (Symtab.make (map swap (Symtab.dest SFC.const_trans_table)));
   10.74  
   10.75  fun invert_const c =
   10.76      case Symtab.lookup const_trans_table_inv c of
   10.77 @@ -167,7 +169,7 @@
   10.78      | Br ("hBOOL",[t]) => term_of_stree [] thy t  (*ignore hBOOL*)
   10.79      | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
   10.80      | Br (a,ts) =>
   10.81 -        case strip_prefix Res_Clause.const_prefix a of
   10.82 +        case strip_prefix SFC.const_prefix a of
   10.83              SOME "equal" =>
   10.84                list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
   10.85            | SOME b =>
   10.86 @@ -181,10 +183,10 @@
   10.87            | NONE => (*a variable, not a constant*)
   10.88                let val T = HOLogic.typeT
   10.89                    val opr = (*a Free variable is typically a Skolem function*)
   10.90 -                    case strip_prefix Res_Clause.fixed_var_prefix a of
   10.91 +                    case strip_prefix SFC.fixed_var_prefix a of
   10.92                          SOME b => Free(b,T)
   10.93                        | NONE =>
   10.94 -                    case strip_prefix Res_Clause.schematic_var_prefix a of
   10.95 +                    case strip_prefix SFC.schematic_var_prefix a of
   10.96                          SOME b => make_var (b,T)
   10.97                        | NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
   10.98                in  list_comb (opr, List.map (term_of_stree [] thy) (ts@args))  end;
   10.99 @@ -194,7 +196,7 @@
  10.100    | constraint_of_stree pol t = case t of
  10.101          Int _ => raise STREE t
  10.102        | Br (a,ts) =>
  10.103 -            (case (strip_prefix Res_Clause.class_prefix a, map type_of_stree ts) of
  10.104 +            (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of
  10.105                   (SOME b, [T]) => (pol, b, T)
  10.106                 | _ => raise STREE t);
  10.107  
  10.108 @@ -444,12 +446,14 @@
  10.109        val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
  10.110        val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
  10.111        val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
  10.112 -      val (ccls,fixes) = Res_Axioms.neg_conjecture_clauses ctxt th sgno
  10.113 +      val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno
  10.114        val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
  10.115        val ccls = map forall_intr_vars ccls
  10.116        val _ =
  10.117 -        if ! Res_Axioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
  10.118 -        else ()
  10.119 +        if ! Sledgehammer_Fact_Preprocessor.trace then
  10.120 +          app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
  10.121 +        else
  10.122 +          ()
  10.123        val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
  10.124        val _ = trace "\ndecode_tstp_file: finishing\n"
  10.125    in