modernized some structure names;
authorwenzelm
Thu Oct 29 16:59:12 2009 +0100 (2009-10-29)
changeset 333166a72af4e84b8
parent 33315 784c1b09d485
child 33317 b4534348b8fd
modernized some structure names;
src/HOL/ATP_Linkup.thy
src/HOL/HOL.thy
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
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/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_blacklist.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Thu Oct 29 16:34:44 2009 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Thu Oct 29 16:59:12 2009 +0100
     1.3 @@ -91,9 +91,9 @@
     1.4  
     1.5  subsection {* Setup of external ATPs *}
     1.6  
     1.7 -use "Tools/res_axioms.ML" setup ResAxioms.setup
     1.8 +use "Tools/res_axioms.ML" setup Res_Axioms.setup
     1.9  use "Tools/res_hol_clause.ML"
    1.10 -use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
    1.11 +use "Tools/res_reconstruct.ML" setup Res_Reconstruct.setup
    1.12  use "Tools/res_atp.ML"
    1.13  
    1.14  use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup
     2.1 --- a/src/HOL/HOL.thy	Thu Oct 29 16:34:44 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Thu Oct 29 16:59:12 2009 +0100
     2.3 @@ -35,7 +35,8 @@
     2.4  begin
     2.5  
     2.6  setup {* Intuitionistic.method_setup @{binding iprover} *}
     2.7 -setup ResBlacklist.setup
     2.8 +
     2.9 +setup Res_Blacklist.setup
    2.10  
    2.11  
    2.12  subsection {* Primitive logic *}
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 29 16:34:44 2009 +0100
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 29 16:59:12 2009 +0100
     3.3 @@ -319,7 +319,7 @@
     3.4      if success then (message, SH_OK (time_isa, time_atp, theorem_names))
     3.5      else (message, SH_FAIL(time_isa, time_atp))
     3.6    end
     3.7 -  handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
     3.8 +  handle Res_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
     3.9         | ERROR msg => ("error: " ^ msg, SH_ERROR)
    3.10         | TimeLimit.TimeOut => ("timeout", SH_ERROR)
    3.11  
     4.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:34:44 2009 +0100
     4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 29 16:59:12 2009 +0100
     4.3 @@ -264,7 +264,7 @@
     4.4              val _ = register birth_time death_time (Thread.self (), desc);
     4.5              val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
     4.6              val message = #message (prover (! timeout) problem)
     4.7 -              handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
     4.8 +              handle Res_HOL_Clause.TOO_TRIVIAL =>   (* FIXME !? *)
     4.9                    "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
    4.10                  | ERROR msg => ("Error: " ^ msg);
    4.11              val _ = unregister message (Thread.self ());
     5.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 29 16:34:44 2009 +0100
     5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 29 16:59:12 2009 +0100
     5.3 @@ -103,7 +103,7 @@
     5.4    let
     5.5      val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
     5.6      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     5.7 -    val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     5.8 +    val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     5.9      val {context = ctxt, facts, goal} = Proof.raw_goal state   (* FIXME ?? *)
    5.10      val problem =
    5.11       {with_full_types = ! ATP_Manager.full_types,
    5.12 @@ -157,7 +157,7 @@
    5.13          (NONE, "Error in prover: " ^ msg)
    5.14      | (Failure, _) =>
    5.15          (NONE, "Failure: No proof with the theorems supplied"))
    5.16 -    handle ResHolClause.TOO_TRIVIAL =>
    5.17 +    handle Res_HOL_Clause.TOO_TRIVIAL =>
    5.18          (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
    5.19        | ERROR msg => (NONE, "Error: " ^ msg)
    5.20    end
     6.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 29 16:34:44 2009 +0100
     6.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Oct 29 16:59:12 2009 +0100
     6.3 @@ -117,8 +117,8 @@
     6.4      (* get clauses and prepare them for writing *)
     6.5      val (ctxt, (chain_ths, th)) = goal;
     6.6      val thy = ProofContext.theory_of ctxt;
     6.7 -    val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths;
     6.8 -    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno);
     6.9 +    val chain_ths = map (Thm.put_name_hint Res_Reconstruct.chained_hint) chain_ths;
    6.10 +    val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoalno);
    6.11      val the_filtered_clauses =
    6.12        (case filtered_clauses of
    6.13          NONE => relevance_filter goal goal_cls
    6.14 @@ -204,14 +204,14 @@
    6.15      val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem;
    6.16    in
    6.17      external_prover
    6.18 -      (ResAtp.get_relevant max_new_clauses insert_theory_const)
    6.19 -      (ResAtp.prepare_clauses false)
    6.20 -      (ResHolClause.tptp_write_file with_full_types)
    6.21 +      (Res_ATP.get_relevant max_new_clauses insert_theory_const)
    6.22 +      (Res_ATP.prepare_clauses false)
    6.23 +      (Res_HOL_Clause.tptp_write_file with_full_types)
    6.24        command
    6.25        (arguments timeout)
    6.26 -      ResReconstruct.find_failure
    6.27 -      (if emit_structured_proof then ResReconstruct.structured_proof
    6.28 -       else ResReconstruct.lemma_list false)
    6.29 +      Res_Reconstruct.find_failure
    6.30 +      (if emit_structured_proof then Res_Reconstruct.structured_proof
    6.31 +       else Res_Reconstruct.lemma_list false)
    6.32        axiom_clauses
    6.33        filtered_clauses
    6.34        name
    6.35 @@ -280,13 +280,13 @@
    6.36      val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
    6.37    in
    6.38      external_prover
    6.39 -      (ResAtp.get_relevant max_new_clauses insert_theory_const)
    6.40 -      (ResAtp.prepare_clauses true)
    6.41 -      (ResHolClause.dfg_write_file with_full_types)
    6.42 +      (Res_ATP.get_relevant max_new_clauses insert_theory_const)
    6.43 +      (Res_ATP.prepare_clauses true)
    6.44 +      (Res_HOL_Clause.dfg_write_file with_full_types)
    6.45        command
    6.46        (arguments timeout)
    6.47 -      ResReconstruct.find_failure
    6.48 -      (ResReconstruct.lemma_list true)
    6.49 +      Res_Reconstruct.find_failure
    6.50 +      (Res_Reconstruct.lemma_list true)
    6.51        axiom_clauses
    6.52        filtered_clauses
    6.53        name
     7.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Oct 29 16:34:44 2009 +0100
     7.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 29 16:59:12 2009 +0100
     7.3 @@ -63,62 +63,62 @@
     7.4  
     7.5  fun metis_lit b c args = (b, (c, args));
     7.6  
     7.7 -fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
     7.8 -  | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
     7.9 -  | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
    7.10 +fun hol_type_to_fol (Res_Clause.AtomV x) = Metis.Term.Var x
    7.11 +  | hol_type_to_fol (Res_Clause.AtomF x) = Metis.Term.Fn(x,[])
    7.12 +  | hol_type_to_fol (Res_Clause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
    7.13  
    7.14  (*These two functions insert type literals before the real literals. That is the
    7.15    opposite order from TPTP linkup, but maybe OK.*)
    7.16  
    7.17  fun hol_term_to_fol_FO tm =
    7.18 -  case ResHolClause.strip_comb tm of
    7.19 -      (ResHolClause.CombConst(c,_,tys), tms) =>
    7.20 +  case Res_HOL_Clause.strip_comb tm of
    7.21 +      (Res_HOL_Clause.CombConst(c,_,tys), tms) =>
    7.22          let val tyargs = map hol_type_to_fol tys
    7.23              val args   = map hol_term_to_fol_FO tms
    7.24          in Metis.Term.Fn (c, tyargs @ args) end
    7.25 -    | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
    7.26 +    | (Res_HOL_Clause.CombVar(v,_), []) => Metis.Term.Var v
    7.27      | _ => error "hol_term_to_fol_FO";
    7.28  
    7.29 -fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a
    7.30 -  | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) =
    7.31 +fun hol_term_to_fol_HO (Res_HOL_Clause.CombVar (a, _)) = Metis.Term.Var a
    7.32 +  | hol_term_to_fol_HO (Res_HOL_Clause.CombConst (a, _, tylist)) =
    7.33        Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    7.34 -  | hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) =
    7.35 +  | hol_term_to_fol_HO (Res_HOL_Clause.CombApp (tm1, tm2)) =
    7.36         Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    7.37  
    7.38  (*The fully-typed translation, to avoid type errors*)
    7.39  fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
    7.40  
    7.41 -fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) =
    7.42 +fun hol_term_to_fol_FT (Res_HOL_Clause.CombVar(a, ty)) =
    7.43        wrap_type (Metis.Term.Var a, ty)
    7.44 -  | hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) =
    7.45 +  | hol_term_to_fol_FT (Res_HOL_Clause.CombConst(a, ty, _)) =
    7.46        wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
    7.47 -  | hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) =
    7.48 +  | hol_term_to_fol_FT (tm as Res_HOL_Clause.CombApp(tm1,tm2)) =
    7.49         wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
    7.50 -                  ResHolClause.type_of_combterm tm);
    7.51 +                  Res_HOL_Clause.type_of_combterm tm);
    7.52  
    7.53 -fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) =
    7.54 -      let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
    7.55 +fun hol_literal_to_fol FO (Res_HOL_Clause.Literal (pol, tm)) =
    7.56 +      let val (Res_HOL_Clause.CombConst(p,_,tys), tms) = Res_HOL_Clause.strip_comb tm
    7.57            val tylits = if p = "equal" then [] else map hol_type_to_fol tys
    7.58            val lits = map hol_term_to_fol_FO tms
    7.59        in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
    7.60 -  | hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) =
    7.61 -     (case ResHolClause.strip_comb tm of
    7.62 -          (ResHolClause.CombConst("equal",_,_), tms) =>
    7.63 +  | hol_literal_to_fol HO (Res_HOL_Clause.Literal (pol, tm)) =
    7.64 +     (case Res_HOL_Clause.strip_comb tm of
    7.65 +          (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
    7.66              metis_lit pol "=" (map hol_term_to_fol_HO tms)
    7.67          | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
    7.68 -  | hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) =
    7.69 -     (case ResHolClause.strip_comb tm of
    7.70 -          (ResHolClause.CombConst("equal",_,_), tms) =>
    7.71 +  | hol_literal_to_fol FT (Res_HOL_Clause.Literal (pol, tm)) =
    7.72 +     (case Res_HOL_Clause.strip_comb tm of
    7.73 +          (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
    7.74              metis_lit pol "=" (map hol_term_to_fol_FT tms)
    7.75          | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
    7.76  
    7.77  fun literals_of_hol_thm thy mode t =
    7.78 -      let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
    7.79 +      let val (lits, types_sorts) = Res_HOL_Clause.literals_of_term thy t
    7.80        in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
    7.81  
    7.82  (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
    7.83 -fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
    7.84 -  | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
    7.85 +fun metis_of_typeLit pos (Res_Clause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
    7.86 +  | metis_of_typeLit pos (Res_Clause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
    7.87  
    7.88  fun default_sort _ (TVar _) = false
    7.89    | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
    7.90 @@ -132,9 +132,9 @@
    7.91               (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
    7.92    in
    7.93        if is_conjecture then
    7.94 -          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
    7.95 +          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), Res_Clause.add_typs types_sorts)
    7.96        else
    7.97 -        let val tylits = ResClause.add_typs
    7.98 +        let val tylits = Res_Clause.add_typs
    7.99                             (filter (not o default_sort ctxt) types_sorts)
   7.100              val mtylits = if Config.get ctxt type_lits
   7.101                            then map (metis_of_typeLit false) tylits else []
   7.102 @@ -145,13 +145,13 @@
   7.103  
   7.104  (* ARITY CLAUSE *)
   7.105  
   7.106 -fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
   7.107 -      metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   7.108 -  | m_arity_cls (ResClause.TVarLit (c,str))     =
   7.109 -      metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
   7.110 +fun m_arity_cls (Res_Clause.TConsLit (c,t,args)) =
   7.111 +      metis_lit true (Res_Clause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   7.112 +  | m_arity_cls (Res_Clause.TVarLit (c,str))     =
   7.113 +      metis_lit false (Res_Clause.make_type_class c) [Metis.Term.Var str];
   7.114  
   7.115  (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   7.116 -fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
   7.117 +fun arity_cls (Res_Clause.ArityClause{conclLit,premLits,...}) =
   7.118    (TrueI,
   7.119     Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   7.120  
   7.121 @@ -160,7 +160,7 @@
   7.122  fun m_classrel_cls subclass superclass =
   7.123    [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   7.124  
   7.125 -fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) =
   7.126 +fun classrel_cls (Res_Clause.ClassrelClause {subclass, superclass, ...}) =
   7.127    (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   7.128  
   7.129  (* ------------------------------------------------------------------------- *)
   7.130 @@ -209,14 +209,14 @@
   7.131    | strip_happ args x = (x, args);
   7.132  
   7.133  fun fol_type_to_isa _ (Metis.Term.Var v) =
   7.134 -     (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of
   7.135 -          SOME w => ResReconstruct.make_tvar w
   7.136 -        | NONE   => ResReconstruct.make_tvar v)
   7.137 +     (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
   7.138 +          SOME w => Res_Reconstruct.make_tvar w
   7.139 +        | NONE   => Res_Reconstruct.make_tvar v)
   7.140    | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   7.141 -     (case ResReconstruct.strip_prefix ResClause.tconst_prefix x of
   7.142 -          SOME tc => Term.Type (ResReconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   7.143 +     (case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix x of
   7.144 +          SOME tc => Term.Type (Res_Reconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   7.145          | NONE    =>
   7.146 -      case ResReconstruct.strip_prefix ResClause.tfree_prefix x of
   7.147 +      case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix x of
   7.148            SOME tf => mk_tfree ctxt tf
   7.149          | NONE    => error ("fol_type_to_isa: " ^ x));
   7.150  
   7.151 @@ -225,10 +225,10 @@
   7.152    let val thy = ProofContext.theory_of ctxt
   7.153        val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
   7.154        fun tm_to_tt (Metis.Term.Var v) =
   7.155 -             (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of
   7.156 -                  SOME w => Type (ResReconstruct.make_tvar w)
   7.157 +             (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
   7.158 +                  SOME w => Type (Res_Reconstruct.make_tvar w)
   7.159                  | NONE =>
   7.160 -              case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of
   7.161 +              case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
   7.162                    SOME w => Term (mk_var (w, HOLogic.typeT))
   7.163                  | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   7.164                      (*Var from Metis with a name like _nnn; possibly a type variable*)
   7.165 @@ -245,14 +245,14 @@
   7.166        and applic_to_tt ("=",ts) =
   7.167              Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
   7.168          | applic_to_tt (a,ts) =
   7.169 -            case ResReconstruct.strip_prefix ResClause.const_prefix a of
   7.170 +            case Res_Reconstruct.strip_prefix Res_Clause.const_prefix a of
   7.171                  SOME b =>
   7.172 -                  let val c = ResReconstruct.invert_const b
   7.173 -                      val ntypes = ResReconstruct.num_typargs thy c
   7.174 +                  let val c = Res_Reconstruct.invert_const b
   7.175 +                      val ntypes = Res_Reconstruct.num_typargs thy c
   7.176                        val nterms = length ts - ntypes
   7.177                        val tts = map tm_to_tt ts
   7.178                        val tys = types_of (List.take(tts,ntypes))
   7.179 -                      val ntyargs = ResReconstruct.num_typargs thy c
   7.180 +                      val ntyargs = Res_Reconstruct.num_typargs thy c
   7.181                    in if length tys = ntyargs then
   7.182                           apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   7.183                       else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
   7.184 @@ -263,14 +263,14 @@
   7.185                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   7.186                       end
   7.187                | NONE => (*Not a constant. Is it a type constructor?*)
   7.188 -            case ResReconstruct.strip_prefix ResClause.tconst_prefix a of
   7.189 +            case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix a of
   7.190                  SOME b =>
   7.191 -                  Type (Term.Type (ResReconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
   7.192 +                  Type (Term.Type (Res_Reconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
   7.193                | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   7.194 -            case ResReconstruct.strip_prefix ResClause.tfree_prefix a of
   7.195 +            case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix a of
   7.196                  SOME b => Type (mk_tfree ctxt b)
   7.197                | NONE => (*a fixed variable? They are Skolem functions.*)
   7.198 -            case ResReconstruct.strip_prefix ResClause.fixed_var_prefix a of
   7.199 +            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix a of
   7.200                  SOME b =>
   7.201                    let val opr = Term.Free(b, HOLogic.typeT)
   7.202                    in  apply_list opr (length ts) (map tm_to_tt ts)  end
   7.203 @@ -281,16 +281,16 @@
   7.204  fun fol_term_to_hol_FT ctxt fol_tm =
   7.205    let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
   7.206        fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
   7.207 -             (case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of
   7.208 +             (case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
   7.209                    SOME w =>  mk_var(w, dummyT)
   7.210                  | NONE   => mk_var(v, dummyT))
   7.211          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
   7.212              Const ("op =", HOLogic.typeT)
   7.213          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   7.214 -           (case ResReconstruct.strip_prefix ResClause.const_prefix x of
   7.215 -                SOME c => Const (ResReconstruct.invert_const c, dummyT)
   7.216 +           (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
   7.217 +                SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
   7.218                | NONE => (*Not a constant. Is it a fixed variable??*)
   7.219 -            case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of
   7.220 +            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
   7.221                  SOME v => Free (v, fol_type_to_isa ctxt ty)
   7.222                | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
   7.223          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   7.224 @@ -301,10 +301,10 @@
   7.225          | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   7.226              list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
   7.227          | cvt (t as Metis.Term.Fn (x, [])) =
   7.228 -           (case ResReconstruct.strip_prefix ResClause.const_prefix x of
   7.229 -                SOME c => Const (ResReconstruct.invert_const c, dummyT)
   7.230 +           (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
   7.231 +                SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
   7.232                | NONE => (*Not a constant. Is it a fixed variable??*)
   7.233 -            case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of
   7.234 +            case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
   7.235                  SOME v => Free (v, dummyT)
   7.236                | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
   7.237                    fol_term_to_hol_RAW ctxt t))
   7.238 @@ -383,9 +383,9 @@
   7.239                                         " in " ^ Display.string_of_thm ctxt i_th);
   7.240                   NONE)
   7.241        fun remove_typeinst (a, t) =
   7.242 -            case ResReconstruct.strip_prefix ResClause.schematic_var_prefix a of
   7.243 +            case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix a of
   7.244                  SOME b => SOME (b, t)
   7.245 -              | NONE   => case ResReconstruct.strip_prefix ResClause.tvar_prefix a of
   7.246 +              | NONE   => case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix a of
   7.247                  SOME _ => NONE          (*type instantiations are forbidden!*)
   7.248                | NONE   => SOME (a,t)    (*internal Metis var?*)
   7.249        val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   7.250 @@ -452,7 +452,7 @@
   7.251    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   7.252  
   7.253  fun get_ty_arg_size _ (Const ("op =", _)) = 0  (*equality has no type arguments*)
   7.254 -  | get_ty_arg_size thy (Const (c, _)) = (ResReconstruct.num_typargs thy c handle TYPE _ => 0)
   7.255 +  | get_ty_arg_size thy (Const (c, _)) = (Res_Reconstruct.num_typargs thy c handle TYPE _ => 0)
   7.256    | get_ty_arg_size _ _ = 0;
   7.257  
   7.258  (* INFERENCE RULE: EQUALITY *)
   7.259 @@ -538,7 +538,7 @@
   7.260    | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
   7.261        equality_inf ctxt mode f_lit f_p f_r;
   7.262  
   7.263 -fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
   7.264 +fun real_literal (_, (c, _)) = not (String.isPrefix Res_Clause.class_prefix c);
   7.265  
   7.266  fun translate _ _ thpairs [] = thpairs
   7.267    | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
   7.268 @@ -564,23 +564,23 @@
   7.269  (* Translation of HO Clauses                                                 *)
   7.270  (* ------------------------------------------------------------------------- *)
   7.271  
   7.272 -fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
   7.273 +fun cnf_th thy th = hd (Res_Axioms.cnf_axiom thy th);
   7.274  
   7.275  val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
   7.276  val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
   7.277  
   7.278 -val comb_I = cnf_th @{theory} ResHolClause.comb_I;
   7.279 -val comb_K = cnf_th @{theory} ResHolClause.comb_K;
   7.280 -val comb_B = cnf_th @{theory} ResHolClause.comb_B;
   7.281 -val comb_C = cnf_th @{theory} ResHolClause.comb_C;
   7.282 -val comb_S = cnf_th @{theory} ResHolClause.comb_S;
   7.283 +val comb_I = cnf_th @{theory} Res_HOL_Clause.comb_I;
   7.284 +val comb_K = cnf_th @{theory} Res_HOL_Clause.comb_K;
   7.285 +val comb_B = cnf_th @{theory} Res_HOL_Clause.comb_B;
   7.286 +val comb_C = cnf_th @{theory} Res_HOL_Clause.comb_C;
   7.287 +val comb_S = cnf_th @{theory} Res_HOL_Clause.comb_S;
   7.288  
   7.289  fun type_ext thy tms =
   7.290 -  let val subs = ResAtp.tfree_classes_of_terms tms
   7.291 -      val supers = ResAtp.tvar_classes_of_terms tms
   7.292 -      and tycons = ResAtp.type_consts_of_terms thy tms
   7.293 -      val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   7.294 -      val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   7.295 +  let val subs = Res_ATP.tfree_classes_of_terms tms
   7.296 +      val supers = Res_ATP.tvar_classes_of_terms tms
   7.297 +      and tycons = Res_ATP.type_consts_of_terms thy tms
   7.298 +      val (supers', arity_clauses) = Res_Clause.make_arity_clauses thy tycons supers
   7.299 +      val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
   7.300    in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   7.301    end;
   7.302  
   7.303 @@ -590,7 +590,7 @@
   7.304  
   7.305  type logic_map =
   7.306    {axioms : (Metis.Thm.thm * thm) list,
   7.307 -   tfrees : ResClause.type_literal list};
   7.308 +   tfrees : Res_Clause.type_literal list};
   7.309  
   7.310  fun const_in_metis c (pred, tm_list) =
   7.311    let
   7.312 @@ -602,7 +602,7 @@
   7.313  (*Extract TFree constraints from context to include as conjecture clauses*)
   7.314  fun init_tfrees ctxt =
   7.315    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
   7.316 -  in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
   7.317 +  in  Res_Clause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
   7.318  
   7.319  (*transform isabelle type / arity clause to metis clause *)
   7.320  fun add_type_thm [] lmap = lmap
   7.321 @@ -664,7 +664,7 @@
   7.322  (* Main function to start metis prove and reconstruction *)
   7.323  fun FOL_SOLVE mode ctxt cls ths0 =
   7.324    let val thy = ProofContext.theory_of ctxt
   7.325 -      val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
   7.326 +      val th_cls_pairs = map (fn th => (Thm.get_name_hint th, Res_Axioms.cnf_axiom thy th)) ths0
   7.327        val ths = maps #2 th_cls_pairs
   7.328        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   7.329        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   7.330 @@ -673,7 +673,7 @@
   7.331        val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
   7.332        val _ = if null tfrees then ()
   7.333                else (trace_msg (fn () => "TFREE CLAUSES");
   7.334 -                    app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
   7.335 +                    app (fn tf => trace_msg (fn _ => Res_Clause.tptp_of_typeLit true tf)) tfrees)
   7.336        val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   7.337        val thms = map #1 axioms
   7.338        val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   7.339 @@ -715,12 +715,12 @@
   7.340    let val _ = trace_msg (fn () =>
   7.341          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   7.342    in
   7.343 -     if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
   7.344 +     if exists_type Res_Axioms.type_has_empty_sort (prop_of st0)
   7.345       then (warning "Proof state contains the empty sort"; Seq.empty)
   7.346       else
   7.347 -       (Meson.MESON ResAxioms.neg_clausify
   7.348 +       (Meson.MESON Res_Axioms.neg_clausify
   7.349           (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
   7.350 -        THEN ResAxioms.expand_defs_tac st0) st0
   7.351 +        THEN Res_Axioms.expand_defs_tac st0) st0
   7.352    end
   7.353    handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
   7.354  
   7.355 @@ -737,7 +737,7 @@
   7.356    method @{binding metisF} FO "METIS for FOL problems" #>
   7.357    method @{binding metisFT} FT "METIS With-fully typed translation" #>
   7.358    Method.setup @{binding finish_clausify}
   7.359 -    (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
   7.360 +    (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
   7.361      "cleanup after conversion to clauses";
   7.362  
   7.363  end;
     8.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 29 16:34:44 2009 +0100
     8.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 29 16:59:12 2009 +0100
     8.3 @@ -11,14 +11,14 @@
     8.4    val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
     8.5      (thm * (string * int)) list
     8.6    val prepare_clauses : bool -> thm list -> thm list ->
     8.7 -    (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
     8.8 -    (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
     8.9 -    ResHolClause.axiom_name vector *
    8.10 -      (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
    8.11 -      ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
    8.12 +    (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list ->
    8.13 +    (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list -> theory ->
    8.14 +    Res_HOL_Clause.axiom_name vector *
    8.15 +      (Res_HOL_Clause.clause list * Res_HOL_Clause.clause list * Res_HOL_Clause.clause list *
    8.16 +      Res_HOL_Clause.clause list * Res_Clause.classrelClause list * Res_Clause.arityClause list)
    8.17  end;
    8.18  
    8.19 -structure ResAtp: RES_ATP =
    8.20 +structure Res_ATP: RES_ATP =
    8.21  struct
    8.22  
    8.23  
    8.24 @@ -238,10 +238,10 @@
    8.25        let val cls = sort compare_pairs newpairs
    8.26            val accepted = List.take (cls, max_new)
    8.27        in
    8.28 -        ResAxioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
    8.29 +        Res_Axioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
    8.30                         ", exceeds the limit of " ^ Int.toString (max_new)));
    8.31 -        ResAxioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    8.32 -        ResAxioms.trace_msg (fn () => "Actually passed: " ^
    8.33 +        Res_Axioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
    8.34 +        Res_Axioms.trace_msg (fn () => "Actually passed: " ^
    8.35            space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
    8.36  
    8.37          (map #1 accepted, map #1 (List.drop (cls, max_new)))
    8.38 @@ -256,7 +256,7 @@
    8.39                  val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
    8.40                  val newp = p + (1.0-p) / convergence
    8.41              in
    8.42 -              ResAxioms.trace_msg (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
    8.43 +              Res_Axioms.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
    8.44                 (map #1 newrels) @ 
    8.45                 (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
    8.46              end
    8.47 @@ -264,12 +264,12 @@
    8.48              let val weight = clause_weight ctab rel_consts consts_typs
    8.49              in
    8.50                if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
    8.51 -              then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
    8.52 +              then (Res_Axioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
    8.53                                              " passes: " ^ Real.toString weight));
    8.54                      relevant ((ax,weight)::newrels, rejects) axs)
    8.55                else relevant (newrels, ax::rejects) axs
    8.56              end
    8.57 -    in  ResAxioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
    8.58 +    in  Res_Axioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
    8.59          relevant ([],[]) 
    8.60      end;
    8.61          
    8.62 @@ -278,12 +278,12 @@
    8.63   then
    8.64    let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
    8.65        val goal_const_tab = get_goal_consts_typs thy goals
    8.66 -      val _ = ResAxioms.trace_msg (fn () => ("Initial constants: " ^
    8.67 +      val _ = Res_Axioms.trace_msg (fn () => ("Initial constants: " ^
    8.68                                   space_implode ", " (Symtab.keys goal_const_tab)));
    8.69        val rels = relevant_clauses max_new thy const_tab (pass_mark) 
    8.70                     goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
    8.71    in
    8.72 -      ResAxioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
    8.73 +      Res_Axioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
    8.74        rels
    8.75    end
    8.76   else axioms;
    8.77 @@ -337,7 +337,7 @@
    8.78  fun make_unique xs =
    8.79    let val ht = mk_clause_table 7000
    8.80    in
    8.81 -      ResAxioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
    8.82 +      Res_Axioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
    8.83        app (ignore o Polyhash.peekInsert ht) xs;
    8.84        Polyhash.listItems ht
    8.85    end;
    8.86 @@ -359,7 +359,7 @@
    8.87      else
    8.88        let val xname = Facts.extern facts name in
    8.89          if Name_Space.is_hidden xname then I
    8.90 -        else cons (xname, filter_out ResAxioms.bad_for_atp ths)
    8.91 +        else cons (xname, filter_out Res_Axioms.bad_for_atp ths)
    8.92        end) facts [];
    8.93  
    8.94  fun all_valid_thms ctxt =
    8.95 @@ -377,7 +377,7 @@
    8.96  
    8.97  (*Ignore blacklisted basenames*)
    8.98  fun add_multi_names (a, ths) pairs =
    8.99 -  if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
   8.100 +  if (Long_Name.base_name a) mem_string Res_Axioms.multi_base_blacklist then pairs
   8.101    else add_single_names (a, ths) pairs;
   8.102  
   8.103  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   8.104 @@ -387,7 +387,7 @@
   8.105    let
   8.106      val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
   8.107      fun blacklisted (_, th) =
   8.108 -      run_blacklist_filter andalso ResBlacklist.blacklisted ctxt th
   8.109 +      run_blacklist_filter andalso Res_Blacklist.blacklisted ctxt th
   8.110    in
   8.111      filter_out blacklisted
   8.112        (fold add_single_names singles (fold add_multi_names mults []))
   8.113 @@ -399,7 +399,7 @@
   8.114  
   8.115  fun get_all_lemmas ctxt =
   8.116    let val included_thms =
   8.117 -        tap (fn ths => ResAxioms.trace_msg
   8.118 +        tap (fn ths => Res_Axioms.trace_msg
   8.119                       (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   8.120              (name_thm_pairs ctxt)
   8.121    in
   8.122 @@ -507,7 +507,7 @@
   8.123      val thy = ProofContext.theory_of ctxt
   8.124      val isFO = isFO thy goal_cls
   8.125      val included_cls = get_all_lemmas ctxt
   8.126 -      |> ResAxioms.cnf_rules_pairs thy |> make_unique
   8.127 +      |> Res_Axioms.cnf_rules_pairs thy |> make_unique
   8.128        |> restrict_to_logic thy isFO
   8.129        |> remove_unwanted_clauses
   8.130    in
   8.131 @@ -520,24 +520,24 @@
   8.132    let
   8.133      (* add chain thms *)
   8.134      val chain_cls =
   8.135 -      ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname chain_ths))
   8.136 +      Res_Axioms.cnf_rules_pairs thy (filter check_named (map Res_Axioms.pairname chain_ths))
   8.137      val axcls = chain_cls @ axcls
   8.138      val extra_cls = chain_cls @ extra_cls
   8.139      val isFO = isFO thy goal_cls
   8.140      val ccls = subtract_cls goal_cls extra_cls
   8.141 -    val _ = app (fn th => ResAxioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   8.142 +    val _ = app (fn th => Res_Axioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   8.143      val ccltms = map prop_of ccls
   8.144      and axtms = map (prop_of o #1) extra_cls
   8.145      val subs = tfree_classes_of_terms ccltms
   8.146      and supers = tvar_classes_of_terms axtms
   8.147      and tycons = type_consts_of_terms thy (ccltms@axtms)
   8.148      (*TFrees in conjecture clauses; TVars in axiom clauses*)
   8.149 -    val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
   8.150 -    val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
   8.151 -    val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
   8.152 -    val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
   8.153 -    val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
   8.154 -    val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   8.155 +    val conjectures = Res_HOL_Clause.make_conjecture_clauses dfg thy ccls
   8.156 +    val (_, extra_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy extra_cls)
   8.157 +    val (clnames,axiom_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy axcls)
   8.158 +    val helper_clauses = Res_HOL_Clause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
   8.159 +    val (supers',arity_clauses) = Res_Clause.make_arity_clauses_dfg dfg thy tycons supers
   8.160 +    val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
   8.161    in
   8.162      (Vector.fromList clnames,
   8.163        (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
     9.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Oct 29 16:34:44 2009 +0100
     9.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 29 16:59:12 2009 +0100
     9.3 @@ -23,7 +23,7 @@
     9.4    val setup: theory -> theory
     9.5  end;
     9.6  
     9.7 -structure ResAxioms: RES_AXIOMS =
     9.8 +structure Res_Axioms: RES_AXIOMS =
     9.9  struct
    9.10  
    9.11  val trace = Unsynchronized.ref false;
    9.12 @@ -286,7 +286,7 @@
    9.13    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
    9.14  
    9.15  
    9.16 -(*** Blacklisting (duplicated in ResAtp?) ***)
    9.17 +(*** Blacklisting (duplicated in Res_ATP?) ***)
    9.18  
    9.19  val max_lambda_nesting = 3;
    9.20  
    9.21 @@ -387,14 +387,14 @@
    9.22  fun cnf_rules_pairs_aux _ pairs [] = pairs
    9.23    | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
    9.24        let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
    9.25 -                       handle THM _ => pairs | ResClause.CLAUSE _ => pairs
    9.26 +                       handle THM _ => pairs | Res_Clause.CLAUSE _ => pairs
    9.27        in  cnf_rules_pairs_aux thy pairs' ths  end;
    9.28  
    9.29  (*The combination of rev and tail recursion preserves the original order*)
    9.30  fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
    9.31  
    9.32  
    9.33 -(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
    9.34 +(**** Convert all facts of the theory into clauses (Res_Clause.clause, or Res_HOL_Clause.clause) ****)
    9.35  
    9.36  local
    9.37  
    10.1 --- a/src/HOL/Tools/res_blacklist.ML	Thu Oct 29 16:34:44 2009 +0100
    10.2 +++ b/src/HOL/Tools/res_blacklist.ML	Thu Oct 29 16:59:12 2009 +0100
    10.3 @@ -16,7 +16,7 @@
    10.4    val del: attribute
    10.5  end;
    10.6  
    10.7 -structure ResBlacklist: RES_BLACKLIST =
    10.8 +structure Res_Blacklist: RES_BLACKLIST =
    10.9  struct
   10.10  
   10.11  structure Data = GenericDataFun
    11.1 --- a/src/HOL/Tools/res_clause.ML	Thu Oct 29 16:34:44 2009 +0100
    11.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Oct 29 16:59:12 2009 +0100
    11.3 @@ -77,7 +77,7 @@
    11.4    val tptp_classrelClause : classrelClause -> string
    11.5  end
    11.6  
    11.7 -structure ResClause: RES_CLAUSE =
    11.8 +structure Res_Clause: RES_CLAUSE =
    11.9  struct
   11.10  
   11.11  val schematic_var_prefix = "V_";
    12.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Oct 29 16:34:44 2009 +0100
    12.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Oct 29 16:59:12 2009 +0100
    12.3 @@ -17,13 +17,13 @@
    12.4    type polarity = bool
    12.5    type clause_id = int
    12.6    datatype combterm =
    12.7 -      CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
    12.8 -    | CombVar of string * ResClause.fol_type
    12.9 +      CombConst of string * Res_Clause.fol_type * Res_Clause.fol_type list (*Const and Free*)
   12.10 +    | CombVar of string * Res_Clause.fol_type
   12.11      | CombApp of combterm * combterm
   12.12    datatype literal = Literal of polarity * combterm
   12.13    datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
   12.14 -                    kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
   12.15 -  val type_of_combterm: combterm -> ResClause.fol_type
   12.16 +                    kind: Res_Clause.kind,literals: literal list, ctypes_sorts: typ list}
   12.17 +  val type_of_combterm: combterm -> Res_Clause.fol_type
   12.18    val strip_comb: combterm -> combterm * combterm list
   12.19    val literals_of_term: theory -> term -> literal list * typ list
   12.20    exception TOO_TRIVIAL
   12.21 @@ -38,18 +38,18 @@
   12.22         clause list
   12.23    val tptp_write_file: bool -> Path.T ->
   12.24      clause list * clause list * clause list * clause list *
   12.25 -    ResClause.classrelClause list * ResClause.arityClause list ->
   12.26 +    Res_Clause.classrelClause list * Res_Clause.arityClause list ->
   12.27      int * int
   12.28    val dfg_write_file: bool -> Path.T ->
   12.29      clause list * clause list * clause list * clause list *
   12.30 -    ResClause.classrelClause list * ResClause.arityClause list ->
   12.31 +    Res_Clause.classrelClause list * Res_Clause.arityClause list ->
   12.32      int * int
   12.33  end
   12.34  
   12.35 -structure ResHolClause: RES_HOL_CLAUSE =
   12.36 +structure Res_HOL_Clause: RES_HOL_CLAUSE =
   12.37  struct
   12.38  
   12.39 -structure RC = ResClause;
   12.40 +structure RC = Res_Clause;   (* FIXME avoid structure alias *)
   12.41  
   12.42  (* theorems for combinators and function extensionality *)
   12.43  val ext = thm "HOL.ext";
   12.44 @@ -404,7 +404,7 @@
   12.45    else ct;
   12.46  
   12.47  fun cnf_helper_thms thy =
   12.48 -  ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
   12.49 +  Res_Axioms.cnf_rules_pairs thy o map Res_Axioms.pairname
   12.50  
   12.51  fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
   12.52    if isFO then []  (*first-order*)
   12.53 @@ -454,7 +454,7 @@
   12.54    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   12.55  
   12.56  fun display_arity const_needs_hBOOL (c,n) =
   12.57 -  ResAxioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
   12.58 +  Res_Axioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
   12.59                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
   12.60  
   12.61  fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
    13.1 --- a/src/HOL/Tools/res_reconstruct.ML	Thu Oct 29 16:34:44 2009 +0100
    13.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Thu Oct 29 16:59:12 2009 +0100
    13.3 @@ -24,13 +24,13 @@
    13.4      string * string vector * (int * int) * Proof.context * thm * int -> string * string list
    13.5  end;
    13.6  
    13.7 -structure ResReconstruct : RES_RECONSTRUCT =
    13.8 +structure Res_Reconstruct : RES_RECONSTRUCT =
    13.9  struct
   13.10  
   13.11  val trace_path = Path.basic "atp_trace";
   13.12  
   13.13  fun trace s =
   13.14 -  if ! ResAxioms.trace then File.append (File.tmp_path trace_path) s
   13.15 +  if ! Res_Axioms.trace then File.append (File.tmp_path trace_path) s
   13.16    else ();
   13.17  
   13.18  fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
   13.19 @@ -107,12 +107,12 @@
   13.20  (*If string s has the prefix s1, return the result of deleting it.*)
   13.21  fun strip_prefix s1 s =
   13.22    if String.isPrefix s1 s
   13.23 -  then SOME (ResClause.undo_ascii_of (String.extract (s, size s1, NONE)))
   13.24 +  then SOME (Res_Clause.undo_ascii_of (String.extract (s, size s1, NONE)))
   13.25    else NONE;
   13.26  
   13.27  (*Invert the table of translations between Isabelle and ATPs*)
   13.28  val type_const_trans_table_inv =
   13.29 -      Symtab.make (map swap (Symtab.dest ResClause.type_const_trans_table));
   13.30 +      Symtab.make (map swap (Symtab.dest Res_Clause.type_const_trans_table));
   13.31  
   13.32  fun invert_type_const c =
   13.33      case Symtab.lookup type_const_trans_table_inv c of
   13.34 @@ -130,15 +130,15 @@
   13.35      | Br (a,ts) =>
   13.36          let val Ts = map type_of_stree ts
   13.37          in
   13.38 -          case strip_prefix ResClause.tconst_prefix a of
   13.39 +          case strip_prefix Res_Clause.tconst_prefix a of
   13.40                SOME b => Type(invert_type_const b, Ts)
   13.41              | NONE =>
   13.42                  if not (null ts) then raise STREE t  (*only tconsts have type arguments*)
   13.43                  else
   13.44 -                case strip_prefix ResClause.tfree_prefix a of
   13.45 +                case strip_prefix Res_Clause.tfree_prefix a of
   13.46                      SOME b => TFree("'" ^ b, HOLogic.typeS)
   13.47                    | NONE =>
   13.48 -                case strip_prefix ResClause.tvar_prefix a of
   13.49 +                case strip_prefix Res_Clause.tvar_prefix a of
   13.50                      SOME b => make_tvar b
   13.51                    | NONE => make_tvar a   (*Variable from the ATP, say X1*)
   13.52          end;
   13.53 @@ -146,7 +146,7 @@
   13.54  (*Invert the table of translations between Isabelle and ATPs*)
   13.55  val const_trans_table_inv =
   13.56        Symtab.update ("fequal", "op =")
   13.57 -        (Symtab.make (map swap (Symtab.dest ResClause.const_trans_table)));
   13.58 +        (Symtab.make (map swap (Symtab.dest Res_Clause.const_trans_table)));
   13.59  
   13.60  fun invert_const c =
   13.61      case Symtab.lookup const_trans_table_inv c of
   13.62 @@ -167,7 +167,7 @@
   13.63      | Br ("hBOOL",[t]) => term_of_stree [] thy t  (*ignore hBOOL*)
   13.64      | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
   13.65      | Br (a,ts) =>
   13.66 -        case strip_prefix ResClause.const_prefix a of
   13.67 +        case strip_prefix Res_Clause.const_prefix a of
   13.68              SOME "equal" =>
   13.69                list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
   13.70            | SOME b =>
   13.71 @@ -181,10 +181,10 @@
   13.72            | NONE => (*a variable, not a constant*)
   13.73                let val T = HOLogic.typeT
   13.74                    val opr = (*a Free variable is typically a Skolem function*)
   13.75 -                    case strip_prefix ResClause.fixed_var_prefix a of
   13.76 +                    case strip_prefix Res_Clause.fixed_var_prefix a of
   13.77                          SOME b => Free(b,T)
   13.78                        | NONE =>
   13.79 -                    case strip_prefix ResClause.schematic_var_prefix a of
   13.80 +                    case strip_prefix Res_Clause.schematic_var_prefix a of
   13.81                          SOME b => make_var (b,T)
   13.82                        | NONE => make_var (a,T)    (*Variable from the ATP, say X1*)
   13.83                in  list_comb (opr, List.map (term_of_stree [] thy) (ts@args))  end;
   13.84 @@ -194,7 +194,7 @@
   13.85    | constraint_of_stree pol t = case t of
   13.86          Int _ => raise STREE t
   13.87        | Br (a,ts) =>
   13.88 -            (case (strip_prefix ResClause.class_prefix a, map type_of_stree ts) of
   13.89 +            (case (strip_prefix Res_Clause.class_prefix a, map type_of_stree ts) of
   13.90                   (SOME b, [T]) => (pol, b, T)
   13.91                 | _ => raise STREE t);
   13.92  
   13.93 @@ -444,11 +444,11 @@
   13.94        val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
   13.95        val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
   13.96        val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
   13.97 -      val (ccls,fixes) = ResAxioms.neg_conjecture_clauses ctxt th sgno
   13.98 +      val (ccls,fixes) = Res_Axioms.neg_conjecture_clauses ctxt th sgno
   13.99        val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
  13.100        val ccls = map forall_intr_vars ccls
  13.101        val _ =
  13.102 -        if ! ResAxioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
  13.103 +        if ! Res_Axioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
  13.104          else ()
  13.105        val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
  13.106        val _ = trace "\ndecode_tstp_file: finishing\n"