renamings + only need second component of name pool to reconstruct proofs
authorblanchet
Wed Jul 21 21:15:07 2010 +0200 (2010-07-21)
changeset 37926e6ff246c0cdb
parent 37925 1188e6bff48d
child 37927 29cacb2c2184
renamings + only need second component of name pool to reconstruct proofs
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
src/HOL/Tools/meson.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Jul 21 21:14:47 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Jul 21 21:15:07 2010 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  signature ATP_MANAGER =
     1.5  sig
     1.6    type relevance_override = Sledgehammer_Fact_Filter.relevance_override
     1.7 -  type name_pool = Sledgehammer_TPTP_Format.name_pool
     1.8    type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
     1.9    type params =
    1.10      {debug: bool,
    1.11 @@ -38,7 +37,7 @@
    1.12    type prover_result =
    1.13      {outcome: failure option,
    1.14       message: string,
    1.15 -     pool: name_pool option,
    1.16 +     pool: string Symtab.table,
    1.17       relevant_thm_names: string list,
    1.18       atp_run_time_in_msecs: int,
    1.19       output: string,
    1.20 @@ -108,7 +107,7 @@
    1.21  type prover_result =
    1.22    {outcome: failure option,
    1.23     message: string,
    1.24 -   pool: name_pool option,
    1.25 +   pool: string Symtab.table,
    1.26     relevant_thm_names: string list,
    1.27     atp_run_time_in_msecs: int,
    1.28     output: string,
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 21:14:47 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Wed Jul 21 21:15:07 2010 +0200
     2.3 @@ -19,7 +19,6 @@
     2.4  structure ATP_Systems : ATP_SYSTEMS =
     2.5  struct
     2.6  
     2.7 -open Clausifier
     2.8  open Metis_Clauses
     2.9  open Sledgehammer_Util
    2.10  open Sledgehammer_Fact_Filter
    2.11 @@ -134,7 +133,7 @@
    2.12    filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
    2.13  
    2.14  fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) =
    2.15 -      (pos andalso c = "c_False") orelse (not pos andalso c = "c_True")
    2.16 +    c = (if pos then "c_False" else "c_True")
    2.17    | is_false_literal _ = false
    2.18  fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) =
    2.19        (pol andalso c = "c_True") orelse
    2.20 @@ -185,7 +184,7 @@
    2.21  
    2.22  fun cnf_helper_thms thy raw =
    2.23    map (`Thm.get_name_hint)
    2.24 -  #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy true)
    2.25 +  #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true)
    2.26  
    2.27  val optional_helpers =
    2.28    [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
    2.29 @@ -256,7 +255,7 @@
    2.30      (* get clauses and prepare them for writing *)
    2.31      val (ctxt, (_, th)) = goal;
    2.32      val thy = ProofContext.theory_of ctxt;
    2.33 -    val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
    2.34 +    val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal)
    2.35      val goal_cls = List.concat goal_clss
    2.36      val the_filtered_clauses =
    2.37        case filtered_clauses of
    2.38 @@ -265,7 +264,7 @@
    2.39                      relevance_convergence defs_relevant max_axiom_clauses
    2.40                      (the_default prefers_theory_relevant theory_relevant)
    2.41                      relevance_override goal goal_cls
    2.42 -                |> cnf_rules_pairs thy true
    2.43 +                |> Clausifier.cnf_rules_pairs thy true
    2.44      val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
    2.45      val (internal_thm_names, clauses) =
    2.46        prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
     3.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:14:47 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:15:07 2010 +0200
     3.3 @@ -75,8 +75,6 @@
     3.4  structure Metis_Clauses : METIS_CLAUSES =
     3.5  struct
     3.6  
     3.7 -open Clausifier
     3.8 -
     3.9  val type_wrapper_name = "ti"
    3.10  
    3.11  val schematic_var_prefix = "V_";
     4.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:14:47 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:15:07 2010 +0200
     4.3 @@ -18,7 +18,6 @@
     4.4  structure Metis_Tactics : METIS_TACTICS =
     4.5  struct
     4.6  
     4.7 -open Clausifier
     4.8  open Metis_Clauses
     4.9  
    4.10  exception METIS of string * string
    4.11 @@ -70,10 +69,10 @@
    4.12  
    4.13  fun metis_lit b c args = (b, (c, args));
    4.14  
    4.15 -fun hol_type_to_fol (CombTVar (x, _)) = Metis.Term.Var x
    4.16 -  | hol_type_to_fol (CombTFree (s, _)) = Metis.Term.Fn (s, [])
    4.17 -  | hol_type_to_fol (CombType ((s, _), tps)) =
    4.18 -    Metis.Term.Fn (s, map hol_type_to_fol tps);
    4.19 +fun metis_term_from_combtyp (CombTVar (s, _)) = Metis.Term.Var s
    4.20 +  | metis_term_from_combtyp (CombTFree (s, _)) = Metis.Term.Fn (s, [])
    4.21 +  | metis_term_from_combtyp (CombType ((s, _), tps)) =
    4.22 +    Metis.Term.Fn (s, map metis_term_from_combtyp tps);
    4.23  
    4.24  (*These two functions insert type literals before the real literals. That is the
    4.25    opposite order from TPTP linkup, but maybe OK.*)
    4.26 @@ -81,7 +80,7 @@
    4.27  fun hol_term_to_fol_FO tm =
    4.28    case strip_combterm_comb tm of
    4.29        (CombConst ((c, _), _, tys), tms) =>
    4.30 -        let val tyargs = map hol_type_to_fol tys
    4.31 +        let val tyargs = map metis_term_from_combtyp tys
    4.32              val args   = map hol_term_to_fol_FO tms
    4.33          in Metis.Term.Fn (c, tyargs @ args) end
    4.34      | (CombVar ((v, _), _), []) => Metis.Term.Var v
    4.35 @@ -89,12 +88,12 @@
    4.36  
    4.37  fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
    4.38    | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
    4.39 -      Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    4.40 +      Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
    4.41    | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
    4.42         Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    4.43  
    4.44  (*The fully-typed translation, to avoid type errors*)
    4.45 -fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
    4.46 +fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
    4.47  
    4.48  fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
    4.49    | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
    4.50 @@ -105,7 +104,7 @@
    4.51  
    4.52  fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
    4.53        let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
    4.54 -          val tylits = if p = "equal" then [] else map hol_type_to_fol tys
    4.55 +          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
    4.56            val lits = map hol_term_to_fol_FO tms
    4.57        in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
    4.58    | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
    4.59 @@ -223,22 +222,23 @@
    4.60  
    4.61  fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
    4.62  
    4.63 -fun fol_type_to_isa _ (Metis.Term.Var v) =
    4.64 +fun hol_type_from_metis_term _ (Metis.Term.Var v) =
    4.65       (case strip_prefix tvar_prefix v of
    4.66            SOME w => make_tvar w
    4.67          | NONE   => make_tvar v)
    4.68 -  | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
    4.69 +  | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
    4.70       (case strip_prefix type_const_prefix x of
    4.71 -          SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys)
    4.72 +          SOME tc => Term.Type (invert_const tc,
    4.73 +                                map (hol_type_from_metis_term ctxt) tys)
    4.74          | NONE    =>
    4.75        case strip_prefix tfree_prefix x of
    4.76            SOME tf => mk_tfree ctxt tf
    4.77 -        | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
    4.78 +        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
    4.79  
    4.80  (*Maps metis terms to isabelle terms*)
    4.81 -fun hol_term_from_fol_PT ctxt fol_tm =
    4.82 +fun hol_term_from_metis_PT ctxt fol_tm =
    4.83    let val thy = ProofContext.theory_of ctxt
    4.84 -      val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
    4.85 +      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
    4.86                                    Metis.Term.toString fol_tm)
    4.87        fun tm_to_tt (Metis.Term.Var v) =
    4.88               (case strip_prefix tvar_prefix v of
    4.89 @@ -298,8 +298,8 @@
    4.90    end
    4.91  
    4.92  (*Maps fully-typed metis terms to isabelle terms*)
    4.93 -fun hol_term_from_fol_FT ctxt fol_tm =
    4.94 -  let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
    4.95 +fun hol_term_from_metis_FT ctxt fol_tm =
    4.96 +  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
    4.97                                    Metis.Term.toString fol_tm)
    4.98        fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
    4.99               (case strip_prefix schematic_var_prefix v of
   4.100 @@ -312,8 +312,8 @@
   4.101                  SOME c => Const (invert_const c, dummyT)
   4.102                | NONE => (*Not a constant. Is it a fixed variable??*)
   4.103              case strip_prefix fixed_var_prefix x of
   4.104 -                SOME v => Free (v, fol_type_to_isa ctxt ty)
   4.105 -              | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
   4.106 +                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
   4.107 +              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
   4.108          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   4.109              cvt tm1 $ cvt tm2
   4.110          | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   4.111 @@ -327,17 +327,17 @@
   4.112                | NONE => (*Not a constant. Is it a fixed variable??*)
   4.113              case strip_prefix fixed_var_prefix x of
   4.114                  SOME v => Free (v, dummyT)
   4.115 -              | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
   4.116 -                  hol_term_from_fol_PT ctxt t))
   4.117 -        | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
   4.118 -            hol_term_from_fol_PT ctxt t)
   4.119 +              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
   4.120 +                  hol_term_from_metis_PT ctxt t))
   4.121 +        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t);
   4.122 +            hol_term_from_metis_PT ctxt t)
   4.123    in fol_tm |> cvt end
   4.124  
   4.125 -fun hol_term_from_fol FT = hol_term_from_fol_FT
   4.126 -  | hol_term_from_fol _ = hol_term_from_fol_PT
   4.127 +fun hol_term_from_metis FT = hol_term_from_metis_FT
   4.128 +  | hol_term_from_metis _ = hol_term_from_metis_PT
   4.129  
   4.130  fun hol_terms_from_fol ctxt mode skolems fol_tms =
   4.131 -  let val ts = map (hol_term_from_fol mode ctxt) fol_tms
   4.132 +  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
   4.133        val _ = trace_msg (fn () => "  calling type inference:")
   4.134        val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   4.135        val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
   4.136 @@ -398,7 +398,7 @@
   4.137        fun subst_translation (x,y) =
   4.138              let val v = find_var x
   4.139                  (* We call "reveal_skolem_terms" and "infer_types" below. *)
   4.140 -                val t = hol_term_from_fol mode ctxt y
   4.141 +                val t = hol_term_from_metis mode ctxt y
   4.142              in  SOME (cterm_of thy (Var v), t)  end
   4.143              handle Option =>
   4.144                  (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   4.145 @@ -599,7 +599,7 @@
   4.146  (* ------------------------------------------------------------------------- *)
   4.147  
   4.148  fun cnf_helper_theorem thy raw th =
   4.149 -  if raw then th else the_single (cnf_axiom thy false th)
   4.150 +  if raw then th else the_single (Clausifier.cnf_axiom thy false th)
   4.151  
   4.152  fun type_ext thy tms =
   4.153    let val subs = tfree_classes_of_terms tms
   4.154 @@ -715,7 +715,7 @@
   4.155  fun FOL_SOLVE mode ctxt cls ths0 =
   4.156    let val thy = ProofContext.theory_of ctxt
   4.157        val th_cls_pairs =
   4.158 -        map (fn th => (Thm.get_name_hint th, cnf_axiom thy false th)) ths0
   4.159 +        map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy false th)) ths0
   4.160        val ths = maps #2 th_cls_pairs
   4.161        val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   4.162        val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   4.163 @@ -774,15 +774,16 @@
   4.164    exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   4.165  
   4.166  fun generic_metis_tac mode ctxt ths i st0 =
   4.167 -  let val _ = trace_msg (fn () =>
   4.168 +  let
   4.169 +    val _ = trace_msg (fn () =>
   4.170          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   4.171    in
   4.172      if exists_type type_has_top_sort (prop_of st0) then
   4.173        (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
   4.174      else
   4.175 -      (Meson.MESON (maps neg_clausify)
   4.176 -                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   4.177 -                   ctxt i) st0
   4.178 +      Meson.MESON (maps Clausifier.neg_clausify)
   4.179 +                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   4.180 +                  ctxt i st0
   4.181       handle ERROR msg => raise METIS ("generic_metis_tac", msg)
   4.182    end
   4.183    handle METIS (loc, msg) =>
   4.184 @@ -800,7 +801,8 @@
   4.185  
   4.186  fun method name mode =
   4.187    Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   4.188 -    SIMPLE_METHOD' (CHANGED_PROP o generic_metis_tac mode ctxt ths)))
   4.189 +      METHOD (fn facts => HEADGOAL (CHANGED_PROP
   4.190 +                                 o generic_metis_tac mode ctxt (facts @ ths)))))
   4.191  
   4.192  val setup =
   4.193    type_lits_setup
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Jul 21 21:14:47 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Jul 21 21:15:07 2010 +0200
     5.3 @@ -18,7 +18,6 @@
     5.4  structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
     5.5  struct
     5.6  
     5.7 -open Clausifier
     5.8  open Metis_Clauses
     5.9  open Sledgehammer_Util
    5.10  open Sledgehammer_Proof_Reconstruct
    5.11 @@ -56,7 +55,7 @@
    5.12      val _ = priority ("Testing " ^ string_of_int num_theorems ^
    5.13                        " theorem" ^ plural_s num_theorems ^ "...")
    5.14      val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
    5.15 -    val axclauses = cnf_rules_pairs thy true name_thm_pairs
    5.16 +    val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_pairs
    5.17      val {context = ctxt, facts, goal} = Proof.goal state
    5.18      val problem =
    5.19       {subgoal = subgoal, goal = (ctxt, (facts, goal)),
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 21 21:14:47 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 21 21:15:07 2010 +0200
     6.3 @@ -17,7 +17,6 @@
     6.4  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
     6.5  struct
     6.6  
     6.7 -open Clausifier
     6.8  open Sledgehammer_Util
     6.9  open Sledgehammer_Fact_Filter
    6.10  open ATP_Manager
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 21 21:14:47 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 21 21:15:07 2010 +0200
     7.3 @@ -8,18 +8,17 @@
     7.4  signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     7.5  sig
     7.6    type minimize_command = string list -> string
     7.7 -  type name_pool = Sledgehammer_TPTP_Format.name_pool
     7.8  
     7.9    val metis_line: bool -> int -> int -> string list -> string
    7.10    val metis_proof_text:
    7.11      bool * minimize_command * string * string vector * thm * int
    7.12      -> string * string list
    7.13    val isar_proof_text:
    7.14 -    name_pool option * bool * int * Proof.context * int list list
    7.15 +    string Symtab.table * bool * int * Proof.context * int list list
    7.16      -> bool * minimize_command * string * string vector * thm * int
    7.17      -> string * string list
    7.18    val proof_text:
    7.19 -    bool -> name_pool option * bool * int * Proof.context * int list list
    7.20 +    bool -> string Symtab.table * bool * int * Proof.context * int list list
    7.21      -> bool * minimize_command * string * string vector * thm * int
    7.22      -> string * string list
    7.23  end;
    7.24 @@ -27,7 +26,6 @@
    7.25  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    7.26  struct
    7.27  
    7.28 -open Clausifier
    7.29  open Metis_Clauses
    7.30  open Sledgehammer_Util
    7.31  open Sledgehammer_Fact_Filter
    7.32 @@ -44,12 +42,6 @@
    7.33  fun is_conjecture_clause_number conjecture_shape num =
    7.34    index_in_shape num conjecture_shape >= 0
    7.35  
    7.36 -fun ugly_name NONE s = s
    7.37 -  | ugly_name (SOME the_pool) s =
    7.38 -    case Symtab.lookup (snd the_pool) s of
    7.39 -      SOME s' => s'
    7.40 -    | NONE => s
    7.41 -
    7.42  fun smart_lambda v t =
    7.43    Abs (case v of
    7.44           Const (s, _) =>
    7.45 @@ -104,7 +96,7 @@
    7.46    | repair_name _ "$false" = "c_False"
    7.47    | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
    7.48    | repair_name _ "equal" = "c_equal" (* probably not needed *)
    7.49 -  | repair_name pool s = ugly_name pool s
    7.50 +  | repair_name pool s = Symtab.lookup pool s |> the_default s
    7.51  (* Generalized first-order terms, which include file names, numbers, etc. *)
    7.52  (* The "x" argument is not strictly necessary, but without it Poly/ML loops
    7.53     forever at compile time. *)
    7.54 @@ -144,12 +136,12 @@
    7.55  fun ints_of_node (IntLeaf n) = cons n
    7.56    | ints_of_node (StrNode (_, us)) = fold ints_of_node us
    7.57  val parse_tstp_annotations =
    7.58 -  Scan.optional ($$ "," |-- parse_term NONE
    7.59 -                   --| Scan.option ($$ "," |-- parse_terms NONE)
    7.60 +  Scan.optional ($$ "," |-- parse_term Symtab.empty
    7.61 +                   --| Scan.option ($$ "," |-- parse_terms Symtab.empty)
    7.62                   >> (fn source => ints_of_node source [])) []
    7.63  
    7.64  fun parse_definition pool =
    7.65 -  $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
    7.66 +  $$ "(" |-- parse_literal pool --| Scan.this_string "<=>"
    7.67    -- parse_clause pool --| $$ ")"
    7.68  
    7.69  (* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:14:47 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:15:07 2010 +0200
     8.3 @@ -10,13 +10,12 @@
     8.4    type class_rel_clause = Metis_Clauses.class_rel_clause
     8.5    type arity_clause = Metis_Clauses.arity_clause
     8.6    type fol_clause = Metis_Clauses.fol_clause
     8.7 -  type name_pool = string Symtab.table * string Symtab.table
     8.8  
     8.9    val write_tptp_file :
    8.10      theory -> bool -> bool -> bool -> Path.T
    8.11      -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
    8.12         * class_rel_clause list * arity_clause list
    8.13 -    -> name_pool option * int
    8.14 +    -> string Symtab.table * int
    8.15  end;
    8.16  
    8.17  structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
    8.18 @@ -56,8 +55,6 @@
    8.19  
    8.20  (** Nice names **)
    8.21  
    8.22 -type name_pool = string Symtab.table * string Symtab.table
    8.23 -
    8.24  fun empty_name_pool readable_names =
    8.25    if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
    8.26  
    8.27 @@ -164,7 +161,7 @@
    8.28    Cnf (hol_ident axiom_name clause_id, kind,
    8.29         atp_literals_for_axiom full_types clause)
    8.30  
    8.31 -fun problem_line_for_class_rel
    8.32 +fun problem_line_for_class_rel_clause
    8.33          (ClassRelClause {axiom_name, subclass, superclass, ...}) =
    8.34    let val ty_arg = ATerm (("T", "T"), []) in
    8.35      Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
    8.36 @@ -176,7 +173,8 @@
    8.37    | atp_literal_for_arity_literal (TVarLit (c, sort)) =
    8.38      (false, ATerm (c, [ATerm (sort, [])]))
    8.39  
    8.40 -fun problem_line_for_arity (ArityClause {axiom_name, conclLit, premLits, ...}) =
    8.41 +fun problem_line_for_arity_clause
    8.42 +        (ArityClause {axiom_name, conclLit, premLits, ...}) =
    8.43    Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
    8.44         map atp_literal_for_arity_literal (conclLit :: premLits))
    8.45  
    8.46 @@ -306,8 +304,9 @@
    8.47                       class_rel_clauses, arity_clauses) =
    8.48    let
    8.49      val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
    8.50 -    val class_rel_lines = map problem_line_for_class_rel class_rel_clauses
    8.51 -    val arity_lines = map problem_line_for_arity arity_clauses
    8.52 +    val class_rel_lines =
    8.53 +      map problem_line_for_class_rel_clause class_rel_clauses
    8.54 +    val arity_lines = map problem_line_for_arity_clause arity_clauses
    8.55      val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
    8.56      val conjecture_lines =
    8.57        map (problem_line_for_conjecture full_types) conjectures
    8.58 @@ -324,6 +323,9 @@
    8.59        length axiom_lines + length class_rel_lines + length arity_lines
    8.60        + length helper_lines
    8.61      val _ = File.write_list file (strings_for_problem problem)
    8.62 -  in (pool, conjecture_offset) end
    8.63 +  in
    8.64 +    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
    8.65 +     conjecture_offset)
    8.66 +  end
    8.67  
    8.68  end;
     9.1 --- a/src/HOL/Tools/meson.ML	Wed Jul 21 21:14:47 2010 +0200
     9.2 +++ b/src/HOL/Tools/meson.ML	Wed Jul 21 21:15:07 2010 +0200
     9.3 @@ -584,8 +584,7 @@
     9.4  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
     9.5  
     9.6  fun skolemize_prems_tac ctxt prems =
     9.7 -    cut_facts_tac (skolemize_nnf_list ctxt prems) THEN'
     9.8 -    REPEAT o (etac exE);
     9.9 +  cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o etac exE
    9.10  
    9.11  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
    9.12    Function mkcl converts theorems to clauses.*)