removed Sledgehammer's support for the DFG syntax;
authorblanchet
Tue Jun 22 14:28:22 2010 +0200 (2010-06-22 ago)
changeset 37498b426cbdb5a23
parent 37497 71fdbffe3275
child 37499 5ff37037fbec
removed Sledgehammer's support for the DFG syntax;
this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/meson_tactic.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.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_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 22 13:17:59 2010 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 22 14:28:22 2010 +0200
     1.3 @@ -341,11 +341,6 @@
     1.4  download page. Sledgehammer requires version 3.5 or above. See
     1.5  \S\ref{installation} for details.
     1.6  
     1.7 -\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that
     1.8 -Sledgehammer communicates with SPASS using the native DFG syntax rather than the
     1.9 -TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided
    1.10 -for compatibility reasons.
    1.11 -
    1.12  \item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
    1.13  Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
    1.14  Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 13:17:59 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 14:28:22 2010 +0200
     2.3 @@ -110,7 +110,7 @@
     2.4  
     2.5  fun shape_of_clauses _ [] = []
     2.6    | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
     2.7 -  | shape_of_clauses j ((lit :: lits) :: clauses) =
     2.8 +  | shape_of_clauses j ((_ :: lits) :: clauses) =
     2.9      let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
    2.10        (j :: hd shape) :: tl shape
    2.11      end
    2.12 @@ -123,7 +123,7 @@
    2.13           : problem) =
    2.14    let
    2.15      (* get clauses and prepare them for writing *)
    2.16 -    val (ctxt, (chained_ths, th)) = goal;
    2.17 +    val (ctxt, (_, th)) = goal;
    2.18      val thy = ProofContext.theory_of ctxt;
    2.19      val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
    2.20      val goal_cls = List.concat goal_clss
    2.21 @@ -136,7 +136,7 @@
    2.22          NONE => the_filtered_clauses
    2.23        | SOME axcls => axcls);
    2.24      val (internal_thm_names, clauses) =
    2.25 -      prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy;
    2.26 +      prepare goal_cls the_axiom_clauses the_filtered_clauses thy
    2.27  
    2.28      (* path to unique problem file *)
    2.29      val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    2.30 @@ -243,16 +243,15 @@
    2.31                  max_axiom_clauses, prefers_theory_relevant})
    2.32          (params as {debug, overlord, full_types, respect_no_atp,
    2.33                      relevance_threshold, relevance_convergence, theory_relevant,
    2.34 -                    defs_relevant, isar_proof, ...})
    2.35 +                    defs_relevant, ...})
    2.36          minimize_command timeout =
    2.37    generic_prover overlord
    2.38        (relevant_facts full_types respect_no_atp relevance_threshold
    2.39                        relevance_convergence defs_relevant max_axiom_clauses
    2.40                        (the_default prefers_theory_relevant theory_relevant))
    2.41 -      (prepare_clauses false full_types)
    2.42 -      (write_tptp_file (debug andalso overlord)) home_var
    2.43 -      executable (arguments timeout) proof_delims known_failures name params
    2.44 -      minimize_command
    2.45 +      (prepare_clauses full_types) (write_tptp_file (debug andalso overlord))
    2.46 +      home_var executable (arguments timeout) proof_delims known_failures name
    2.47 +      params minimize_command
    2.48  
    2.49  fun tptp_prover name p = (name, generic_tptp_prover (name, p));
    2.50  
    2.51 @@ -313,31 +312,14 @@
    2.52  
    2.53  (* SPASS *)
    2.54  
    2.55 -fun generic_dfg_prover
    2.56 -        (name, {home_var, executable, arguments, proof_delims, known_failures,
    2.57 -                max_axiom_clauses, prefers_theory_relevant})
    2.58 -        (params as {overlord, full_types, respect_no_atp, relevance_threshold,
    2.59 -                    relevance_convergence, theory_relevant, defs_relevant, ...})
    2.60 -        minimize_command timeout =
    2.61 -  generic_prover overlord
    2.62 -      (relevant_facts full_types respect_no_atp relevance_threshold
    2.63 -                      relevance_convergence defs_relevant max_axiom_clauses
    2.64 -                      (the_default prefers_theory_relevant theory_relevant))
    2.65 -      (prepare_clauses true full_types) write_dfg_file home_var executable
    2.66 -      (arguments timeout) proof_delims known_failures name params
    2.67 -      minimize_command
    2.68 -
    2.69 -fun dfg_prover name p = (name, generic_dfg_prover (name, p))
    2.70 -
    2.71  (* The "-VarWeight=3" option helps the higher-order problems, probably by
    2.72     counteracting the presence of "hAPP". *)
    2.73 -fun generic_spass_config dfg : prover_config =
    2.74 +val spass_config : prover_config =
    2.75    {home_var = "SPASS_HOME",
    2.76     executable = "SPASS",
    2.77     arguments = fn timeout =>
    2.78 -     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    2.79 -     \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)
    2.80 -     |> not dfg ? prefix "-TPTP ",
    2.81 +     "-TPTP -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    2.82 +     \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
    2.83     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    2.84     known_failures =
    2.85       [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
    2.86 @@ -349,10 +331,6 @@
    2.87        (OldSpass, "Unrecognized option TPTP")],
    2.88     max_axiom_clauses = 40,
    2.89     prefers_theory_relevant = true}
    2.90 -val spass_dfg_config = generic_spass_config true
    2.91 -val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
    2.92 -
    2.93 -val spass_config = generic_spass_config false
    2.94  val spass = tptp_prover "spass" spass_config
    2.95  
    2.96  (* remote prover invocation via SystemOnTPTP *)
    2.97 @@ -414,8 +392,7 @@
    2.98    space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
    2.99                       remotify (fst vampire)]
   2.100  
   2.101 -val provers =
   2.102 -  [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
   2.103 +val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e]
   2.104  val prover_setup = fold add_prover provers
   2.105  
   2.106  val setup =
     3.1 --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Tue Jun 22 13:17:59 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Tue Jun 22 14:28:22 2010 +0200
     3.3 @@ -17,11 +17,11 @@
     3.4  open Sledgehammer_Fact_Preprocessor
     3.5  
     3.6  (*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
     3.7 -fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
     3.8 +fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
     3.9      String.isPrefix skolem_prefix a
    3.10    | is_absko _ = false;
    3.11  
    3.12 -fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) =   (*Definition of Free, not in certain terms*)
    3.13 +fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) =   (*Definition of Free, not in certain terms*)
    3.14        is_Free t andalso not (member (op aconv) xs t)
    3.15    | is_okdef _ _ = false
    3.16  
     4.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 22 13:17:59 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 22 14:28:22 2010 +0200
     4.3 @@ -58,7 +58,7 @@
     4.4  (* Finding the relative location of an untyped term within a list of terms *)
     4.5  fun get_index lit =
     4.6    let val lit = Envir.eta_contract lit
     4.7 -      fun get n [] = raise Empty
     4.8 +      fun get _ [] = raise Empty
     4.9          | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    4.10                            then n  else get (n+1) xs
    4.11    in get 1 end;
    4.12 @@ -238,7 +238,7 @@
    4.13          | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
    4.14  
    4.15  fun reveal_skolem_somes skolem_somes =
    4.16 -  map_aterms (fn t as Const (s, T) =>
    4.17 +  map_aterms (fn t as Const (s, _) =>
    4.18                   if String.isPrefix skolem_theory_name s then
    4.19                     AList.lookup (op =) skolem_somes s
    4.20                     |> the |> map_types Type_Infer.paramify_vars
    4.21 @@ -348,8 +348,7 @@
    4.22    | hol_term_from_fol _ = hol_term_from_fol_PT
    4.23  
    4.24  fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
    4.25 -  let val thy = ProofContext.theory_of ctxt
    4.26 -      val ts = map (hol_term_from_fol mode ctxt) fol_tms
    4.27 +  let val ts = map (hol_term_from_fol mode ctxt) fol_tms
    4.28        val _ = trace_msg (fn () => "  calling type inference:")
    4.29        val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
    4.30        val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
    4.31 @@ -694,11 +693,10 @@
    4.32              tfrees = union (op =) tfree_lits tfrees,
    4.33              skolem_somes = skolem_somes}
    4.34          end;
    4.35 -      val lmap as {skolem_somes, ...} =
    4.36 -        {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
    4.37 -        |> fold (add_thm true) cls
    4.38 -        |> add_tfrees
    4.39 -        |> fold (add_thm false) ths
    4.40 +      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
    4.41 +                 |> fold (add_thm true) cls
    4.42 +                 |> add_tfrees
    4.43 +                 |> fold (add_thm false) ths
    4.44        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
    4.45        fun is_used c =
    4.46          exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 13:17:59 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 14:28:22 2010 +0200
     5.3 @@ -27,8 +27,7 @@
     5.4      -> Proof.context * (thm list * 'a) -> thm list
     5.5      -> (thm * (string * int)) list
     5.6    val prepare_clauses :
     5.7 -    bool -> bool -> thm list -> thm list
     5.8 -    -> (thm * (axiom_name * hol_clause_id)) list
     5.9 +    bool -> thm list -> (thm * (axiom_name * hol_clause_id)) list
    5.10      -> (thm * (axiom_name * hol_clause_id)) list -> theory
    5.11      -> axiom_name vector
    5.12         * (hol_clause list * hol_clause list * hol_clause list *
    5.13 @@ -265,7 +264,7 @@
    5.14    end
    5.15  
    5.16  fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
    5.17 -                     (relevance_override as {add, del, only}) ctab =
    5.18 +                     ({add, del, ...} : relevance_override) ctab =
    5.19    let
    5.20      val thy = ProofContext.theory_of ctxt
    5.21      val add_thms = cnf_for_facts ctxt add
    5.22 @@ -398,7 +397,7 @@
    5.23  fun multi_name a th (n, pairs) =
    5.24    (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
    5.25  
    5.26 -fun add_names (a, []) pairs = pairs
    5.27 +fun add_names (_, []) pairs = pairs
    5.28    | add_names (a, [th]) pairs = (a, th) :: pairs
    5.29    | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
    5.30  
    5.31 @@ -478,7 +477,7 @@
    5.32  (*Ensures that no higher-order theorems "leak out"*)
    5.33  fun restrict_to_logic thy true cls =
    5.34      filter (is_quasi_fol_term thy o prop_of o fst) cls
    5.35 -  | restrict_to_logic thy false cls = cls;
    5.36 +  | restrict_to_logic _ false cls = cls
    5.37  
    5.38  (**** Predicates to detect unwanted clauses (prolific or likely to cause
    5.39        unsoundness) ****)
    5.40 @@ -566,7 +565,7 @@
    5.41  
    5.42  (* prepare for passing to writer,
    5.43     create additional clauses based on the information from extra_cls *)
    5.44 -fun prepare_clauses dfg full_types goal_cls chained_ths axcls extra_cls thy =
    5.45 +fun prepare_clauses full_types goal_cls axcls extra_cls thy =
    5.46    let
    5.47      val is_FO = is_fol_goal thy goal_cls
    5.48      val ccls = subtract_cls extra_cls goal_cls
    5.49 @@ -577,12 +576,12 @@
    5.50      and supers = tvar_classes_of_terms axtms
    5.51      and tycons = type_consts_of_terms thy (ccltms @ axtms)
    5.52      (*TFrees in conjecture clauses; TVars in axiom clauses*)
    5.53 -    val conjectures = make_conjecture_clauses dfg thy ccls
    5.54 -    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
    5.55 -    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
    5.56 +    val conjectures = make_conjecture_clauses thy ccls
    5.57 +    val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
    5.58 +    val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
    5.59      val helper_clauses =
    5.60 -      get_helper_clauses dfg thy is_FO full_types conjectures extra_cls
    5.61 -    val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
    5.62 +      get_helper_clauses thy is_FO full_types conjectures extra_cls
    5.63 +    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
    5.64      val classrel_clauses = make_classrel_clauses thy subs supers'
    5.65    in
    5.66      (Vector.fromList clnames,
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jun 22 13:17:59 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jun 22 14:28:22 2010 +0200
     6.3 @@ -47,8 +47,8 @@
     6.4  fun string_for_outcome NONE = "Success."
     6.5    | string_for_outcome (SOME failure) = string_for_failure failure
     6.6  
     6.7 -fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
     6.8 -        timeout subgoal state filtered_clauses name_thms_pairs =
     6.9 +fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
    6.10 +                               filtered_clauses name_thms_pairs =
    6.11    let
    6.12      val num_theorems = length name_thms_pairs
    6.13      val _ = priority ("Testing " ^ string_of_int num_theorems ^
    6.14 @@ -88,7 +88,7 @@
    6.15          (result as {outcome = NONE, ...}) => SOME result
    6.16        | _ => NONE
    6.17  
    6.18 -    val {context = ctxt, facts, goal} = Proof.goal state;
    6.19 +    val {context = ctxt, goal, ...} = Proof.goal state;
    6.20    in
    6.21      (* try prove first to check result and get used theorems *)
    6.22      (case test_thms_fun NONE name_thms_pairs of
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 13:17:59 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 14:28:22 2010 +0200
     7.3 @@ -21,9 +21,8 @@
     7.4    val cnf_rules_pairs:
     7.5      theory -> (string * thm) list -> (thm * (string * int)) list
     7.6    val saturate_skolem_cache: theory -> theory option
     7.7 -  val use_skolem_cache: bool Unsynchronized.ref
     7.8 +  val auto_saturate_skolem_cache: bool Unsynchronized.ref
     7.9      (* for emergency use where the Skolem cache causes problems *)
    7.10 -  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
    7.11    val neg_clausify: thm -> thm list
    7.12    val neg_conjecture_clauses:
    7.13      Proof.context -> thm -> int -> thm list list * (string * typ) list
    7.14 @@ -133,7 +132,7 @@
    7.15        | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
    7.16        | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
    7.17        | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
    7.18 -      | dec_sko t thx = thx
    7.19 +      | dec_sko _ thx = thx
    7.20    in dec_sko (prop_of th) ([], thy) end
    7.21  
    7.22  fun mk_skolem_id t =
    7.23 @@ -168,7 +167,7 @@
    7.24        | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
    7.25        | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
    7.26        | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
    7.27 -      | dec_sko t defs = defs (*Do nothing otherwise*)
    7.28 +      | dec_sko _ defs = defs
    7.29    in  dec_sko (prop_of th) []  end;
    7.30  
    7.31  
    7.32 @@ -520,22 +519,11 @@
    7.33  
    7.34  end;
    7.35  
    7.36 -val use_skolem_cache = Unsynchronized.ref true
    7.37 -
    7.38 -fun clause_cache_endtheory thy =
    7.39 -  if !use_skolem_cache then saturate_skolem_cache thy else NONE
    7.40 -
    7.41 +val auto_saturate_skolem_cache = Unsynchronized.ref true
    7.42  
    7.43 -(* The cache can be kept smaller by inspecting the prop of each thm. Can ignore
    7.44 -   all that are quasi-lambda-free, but then the individual theory caches become
    7.45 -   much bigger. *)
    7.46 +fun conditionally_saturate_skolem_cache thy =
    7.47 +  if !auto_saturate_skolem_cache then saturate_skolem_cache thy else NONE
    7.48  
    7.49 -fun strip_subgoal goal i =
    7.50 -  let
    7.51 -    val (t, frees) = Logic.goal_params (prop_of goal) i
    7.52 -    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
    7.53 -    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    7.54 -  in (rev (map dest_Free frees), hyp_ts, concl_t) end
    7.55  
    7.56  (*** Converting a subgoal into negated conjecture clauses. ***)
    7.57  
    7.58 @@ -574,7 +562,7 @@
    7.59  (** setup **)
    7.60  
    7.61  val setup =
    7.62 -  perhaps saturate_skolem_cache
    7.63 -  #> Theory.at_end clause_cache_endtheory
    7.64 +  perhaps conditionally_saturate_skolem_cache
    7.65 +  #> Theory.at_end conditionally_saturate_skolem_cache
    7.66  
    7.67  end;
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 13:17:59 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 14:28:22 2010 +0200
     8.3 @@ -28,8 +28,8 @@
     8.4    val make_fixed_var : string -> string
     8.5    val make_schematic_type_var : string * int -> string
     8.6    val make_fixed_type_var : string -> string
     8.7 -  val make_fixed_const : bool -> string -> string
     8.8 -  val make_fixed_type_const : bool -> string -> string
     8.9 +  val make_fixed_const : string -> string
    8.10 +  val make_fixed_type_const : string -> string
    8.11    val make_type_class : string -> string
    8.12    type name = string * string
    8.13    type name_pool = string Symtab.table * string Symtab.table
    8.14 @@ -49,7 +49,6 @@
    8.15      TyLitFree of string * name
    8.16    exception CLAUSE of string * term
    8.17    val type_literals_for_types : typ list -> type_literal list
    8.18 -  val get_tvar_strs: typ list -> string list
    8.19    datatype arLit =
    8.20        TConsLit of class * string * string list
    8.21      | TVarLit of class * string
    8.22 @@ -58,28 +57,7 @@
    8.23    datatype classrel_clause = ClassrelClause of
    8.24     {axiom_name: axiom_name, subclass: class, superclass: class}
    8.25    val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
    8.26 -  val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list
    8.27    val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    8.28 -  val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table
    8.29 -  val add_classrel_clause_preds :
    8.30 -    classrel_clause -> int Symtab.table -> int Symtab.table
    8.31 -  val class_of_arityLit: arLit -> class
    8.32 -  val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table
    8.33 -  val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table
    8.34 -  val add_arity_clause_funcs:
    8.35 -    arity_clause -> int Symtab.table -> int Symtab.table
    8.36 -  val init_functab: int Symtab.table
    8.37 -  val dfg_sign: bool -> string -> string
    8.38 -  val dfg_of_type_literal: bool -> type_literal -> string
    8.39 -  val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    8.40 -  val string_of_preds: (string * Int.int) list -> string
    8.41 -  val string_of_funcs: (string * int) list -> string
    8.42 -  val string_of_symbols: string -> string -> string
    8.43 -  val string_of_start: string -> string
    8.44 -  val string_of_descrip : string -> string
    8.45 -  val dfg_tfree_clause : string -> string
    8.46 -  val dfg_classrel_clause: classrel_clause -> string
    8.47 -  val dfg_arity_clause: arity_clause -> string
    8.48    val tptp_sign: bool -> string -> string
    8.49    val tptp_of_type_literal :
    8.50      bool -> type_literal -> name_pool option -> string * name_pool option
    8.51 @@ -196,31 +174,21 @@
    8.52        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
    8.53  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
    8.54  
    8.55 -val max_dfg_symbol_length = 63
    8.56 -
    8.57 -(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
    8.58 -fun controlled_length dfg s =
    8.59 -  if dfg andalso size s > max_dfg_symbol_length then
    8.60 -    String.extract (s, 0, SOME (max_dfg_symbol_length div 2 - 1)) ^ "__" ^
    8.61 -    String.extract (s, size s - max_dfg_symbol_length div 2 + 1, NONE)
    8.62 -  else
    8.63 -    s
    8.64 +fun lookup_const c =
    8.65 +  case Symtab.lookup const_trans_table c of
    8.66 +    SOME c' => c'
    8.67 +  | NONE => ascii_of c
    8.68  
    8.69 -fun lookup_const dfg c =
    8.70 -    case Symtab.lookup const_trans_table c of
    8.71 -        SOME c' => c'
    8.72 -      | NONE => controlled_length dfg (ascii_of c);
    8.73 -
    8.74 -fun lookup_type_const dfg c =
    8.75 -    case Symtab.lookup type_const_trans_table c of
    8.76 -        SOME c' => c'
    8.77 -      | NONE => controlled_length dfg (ascii_of c);
    8.78 +fun lookup_type_const c =
    8.79 +  case Symtab.lookup type_const_trans_table c of
    8.80 +    SOME c' => c'
    8.81 +  | NONE => ascii_of c
    8.82  
    8.83  (* "op =" MUST BE "equal" because it's built into ATPs. *)
    8.84 -fun make_fixed_const _ (@{const_name "op ="}) = "equal"
    8.85 -  | make_fixed_const dfg c = const_prefix ^ lookup_const dfg c;
    8.86 +fun make_fixed_const @{const_name "op ="} = "equal"
    8.87 +  | make_fixed_const c = const_prefix ^ lookup_const c
    8.88  
    8.89 -fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c;
    8.90 +fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c
    8.91  
    8.92  fun make_type_class clas = class_prefix ^ ascii_of clas;
    8.93  
    8.94 @@ -287,8 +255,7 @@
    8.95                              the_pool
    8.96                |> apsnd SOME
    8.97  
    8.98 -(**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG
    8.99 -      format ****)
   8.100 +(**** Definitions and functions for FOL clauses for TPTP format output ****)
   8.101  
   8.102  datatype kind = Axiom | Conjecture;
   8.103  
   8.104 @@ -329,30 +296,12 @@
   8.105  fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   8.106    | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
   8.107  
   8.108 -fun pred_of_sort (TyLitVar (s, _)) = (s, 1)
   8.109 -  | pred_of_sort (TyLitFree (s, _)) = (s, 1)
   8.110 -
   8.111  (*Given a list of sorted type variables, return a list of type literals.*)
   8.112  fun type_literals_for_types Ts =
   8.113    fold (union (op =)) (map sorts_on_typs Ts) []
   8.114  
   8.115 -(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   8.116 -  *  Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
   8.117 -    in a lemma has the same sort as 'a in the conjecture.
   8.118 -  * Deleting such clauses will lead to problems with locales in other use of local results
   8.119 -    where 'a is fixed. Probably we should delete clauses unless the sorts agree.
   8.120 -  * Currently we include a class constraint in the clause, exactly as with TVars.
   8.121 -*)
   8.122 -
   8.123  (** make axiom and conjecture clauses. **)
   8.124  
   8.125 -fun get_tvar_strs [] = []
   8.126 -  | get_tvar_strs ((TVar (indx,s))::Ts) =
   8.127 -      insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts)
   8.128 -  | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts
   8.129 -
   8.130 -
   8.131 -
   8.132  (**** Isabelle arities ****)
   8.133  
   8.134  datatype arLit = TConsLit of class * string * string list
   8.135 @@ -372,13 +321,13 @@
   8.136    | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
   8.137  
   8.138  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
   8.139 -fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) =
   8.140 +fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
   8.141     let val tvars = gen_TVars (length args)
   8.142         val tvars_srts = ListPair.zip (tvars,args)
   8.143     in
   8.144 -      ArityClause {axiom_name = axiom_name, 
   8.145 -                   conclLit = TConsLit (cls, make_fixed_type_const dfg tcons, tvars),
   8.146 -                   premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   8.147 +     ArityClause {axiom_name = axiom_name, 
   8.148 +                  conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
   8.149 +                  premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   8.150     end;
   8.151  
   8.152  
   8.153 @@ -390,7 +339,7 @@
   8.154                              superclass: class};
   8.155  
   8.156  (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   8.157 -fun class_pairs thy [] supers = []
   8.158 +fun class_pairs _ [] _ = []
   8.159    | class_pairs thy subs supers =
   8.160        let
   8.161          val class_less = Sorts.class_less (Sign.classes_of thy)
   8.162 @@ -409,20 +358,20 @@
   8.163  
   8.164  (** Isabelle arities **)
   8.165  
   8.166 -fun arity_clause dfg _ _ (tcons, []) = []
   8.167 -  | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   8.168 -      arity_clause dfg seen n (tcons,ars)
   8.169 -  | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) =
   8.170 +fun arity_clause _ _ (_, []) = []
   8.171 +  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   8.172 +      arity_clause seen n (tcons,ars)
   8.173 +  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   8.174        if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
   8.175 -          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   8.176 -          arity_clause dfg seen (n+1) (tcons,ars)
   8.177 +          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   8.178 +          arity_clause seen (n+1) (tcons,ars)
   8.179        else
   8.180 -          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) ::
   8.181 -          arity_clause dfg (class::seen) n (tcons,ars)
   8.182 +          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
   8.183 +          arity_clause (class::seen) n (tcons,ars)
   8.184  
   8.185 -fun multi_arity_clause dfg [] = []
   8.186 -  | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) =
   8.187 -      arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists
   8.188 +fun multi_arity_clause [] = []
   8.189 +  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   8.190 +      arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   8.191  
   8.192  (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   8.193    provided its arguments have the corresponding sorts.*)
   8.194 @@ -436,7 +385,7 @@
   8.195    in  map try_classes tycons  end;
   8.196  
   8.197  (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   8.198 -fun iter_type_class_pairs thy tycons [] = ([], [])
   8.199 +fun iter_type_class_pairs _ _ [] = ([], [])
   8.200    | iter_type_class_pairs thy tycons classes =
   8.201        let val cpairs = type_class_pairs thy tycons classes
   8.202            val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
   8.203 @@ -444,130 +393,16 @@
   8.204            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   8.205        in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   8.206  
   8.207 -fun make_arity_clauses_dfg dfg thy tycons classes =
   8.208 +fun make_arity_clauses thy tycons classes =
   8.209    let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   8.210 -  in  (classes', multi_arity_clause dfg cpairs)  end;
   8.211 -val make_arity_clauses = make_arity_clauses_dfg false;
   8.212 -
   8.213 -(**** Find occurrences of predicates in clauses ****)
   8.214 -
   8.215 -(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
   8.216 -  function (it flags repeated declarations of a function, even with the same arity)*)
   8.217 -
   8.218 -fun update_many keypairs = fold Symtab.update keypairs
   8.219 -
   8.220 -val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs
   8.221 -
   8.222 -fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) =
   8.223 -  Symtab.update (subclass, 1) #> Symtab.update (superclass, 1)
   8.224 -
   8.225 -fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
   8.226 -  | class_of_arityLit (TVarLit (tclass, _)) = tclass;
   8.227 -
   8.228 -fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) =
   8.229 -  let
   8.230 -    val classes = map (make_type_class o class_of_arityLit)
   8.231 -                      (conclLit :: premLits)
   8.232 -  in fold (Symtab.update o rpair 1) classes end;
   8.233 -
   8.234 -(*** Find occurrences of functions in clauses ***)
   8.235 -
   8.236 -fun add_fol_type_funcs (TyVar _) = I
   8.237 -  | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0)
   8.238 -  | add_fol_type_funcs (TyConstr ((s, _), tys)) =
   8.239 -    Symtab.update (s, length tys) #> fold add_fol_type_funcs tys
   8.240 -
   8.241 -(*TFrees are recorded as constants*)
   8.242 -fun add_type_sort_funcs (TVar _, funcs) = funcs
   8.243 -  | add_type_sort_funcs (TFree (a, _), funcs) =
   8.244 -      Symtab.update (make_fixed_type_var a, 0) funcs
   8.245 -
   8.246 -fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs =
   8.247 -  let val TConsLit (_, tcons, tvars) = conclLit
   8.248 -  in  Symtab.update (tcons, length tvars) funcs  end;
   8.249 -
   8.250 -(*This type can be overlooked because it is built-in...*)
   8.251 -val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty;
   8.252 -
   8.253 -
   8.254 -(**** String-oriented operations ****)
   8.255 -
   8.256 -fun string_of_clausename (cls_id,ax_name) =
   8.257 -    clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   8.258 -
   8.259 -fun string_of_type_clsname (cls_id,ax_name,idx) =
   8.260 -    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   8.261 -
   8.262 -
   8.263 -(**** Producing DFG files ****)
   8.264 -
   8.265 -(*Attach sign in DFG syntax: false means negate.*)
   8.266 -fun dfg_sign true s = s
   8.267 -  | dfg_sign false s = "not(" ^ s ^ ")"
   8.268 -
   8.269 -fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) =
   8.270 -    dfg_sign pos (s ^ "(" ^ s' ^ ")")
   8.271 -  | dfg_of_type_literal pos (TyLitFree (s, (s', _))) =
   8.272 -    dfg_sign pos (s ^ "(" ^ s' ^ ")");
   8.273 -
   8.274 -(*Enclose the clause body by quantifiers, if necessary*)
   8.275 -fun dfg_forall [] body = body
   8.276 -  | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
   8.277 -
   8.278 -fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) =
   8.279 -      "clause( %(axiom)\n" ^
   8.280 -      dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^
   8.281 -      string_of_clausename (cls_id,ax_name) ^  ").\n\n"
   8.282 -  | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) =
   8.283 -      "clause( %(negated_conjecture)\n" ^
   8.284 -      dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
   8.285 -      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   8.286 -
   8.287 -fun string_of_arity (name, arity) =  "(" ^ name ^ ", " ^ Int.toString arity ^ ")"
   8.288 -
   8.289 -fun string_of_preds [] = ""
   8.290 -  | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
   8.291 -
   8.292 -fun string_of_funcs [] = ""
   8.293 -  | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
   8.294 -
   8.295 -fun string_of_symbols predstr funcstr =
   8.296 -  "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   8.297 -
   8.298 -fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
   8.299 -
   8.300 -fun string_of_descrip name =
   8.301 -  "list_of_descriptions.\nname({*" ^ name ^
   8.302 -  "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   8.303 -
   8.304 -fun dfg_tfree_clause tfree_lit =
   8.305 -  "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   8.306 -
   8.307 -fun dfg_of_arLit (TConsLit (c,t,args)) =
   8.308 -      dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   8.309 -  | dfg_of_arLit (TVarLit (c,str)) =
   8.310 -      dfg_sign false (make_type_class c ^ "(" ^ str ^ ")")
   8.311 -
   8.312 -fun dfg_classrelLits sub sup =  "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
   8.313 -
   8.314 -fun dfg_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   8.315 -  "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
   8.316 -  axiom_name ^ ").\n\n";
   8.317 -
   8.318 -fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
   8.319 -
   8.320 -fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   8.321 -  let val TConsLit (_,_,tvars) = conclLit
   8.322 -      val lits = map dfg_of_arLit (conclLit :: premLits)
   8.323 -  in
   8.324 -      "clause( %(axiom)\n" ^
   8.325 -      dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
   8.326 -      string_of_ar axiom_name ^ ").\n\n"
   8.327 -  end;
   8.328 +  in  (classes', multi_arity_clause cpairs)  end;
   8.329  
   8.330  
   8.331  (**** Produce TPTP files ****)
   8.332  
   8.333 +fun string_of_clausename (cls_id, ax_name) =
   8.334 +    clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id
   8.335 +
   8.336  fun tptp_sign true s = s
   8.337    | tptp_sign false s = "~ " ^ s
   8.338  
   8.339 @@ -594,8 +429,8 @@
   8.340    | tptp_of_arLit (TVarLit (c,str)) =
   8.341        tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   8.342  
   8.343 -fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   8.344 -  tptp_cnf (string_of_ar axiom_name) "axiom"
   8.345 +fun tptp_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) =
   8.346 +  tptp_cnf (arclause_prefix ^ ascii_of axiom_name) "axiom"
   8.347             (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
   8.348  
   8.349  fun tptp_classrelLits sub sup =
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 13:17:59 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 14:28:22 2010 +0200
     9.3 @@ -32,19 +32,17 @@
     9.4    val conceal_skolem_somes :
     9.5      int -> (string * term) list -> term -> (string * term) list * term
     9.6    exception TRIVIAL
     9.7 -  val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
     9.8 -  val make_axiom_clauses : bool -> theory ->
     9.9 -       (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
    9.10 +  val make_conjecture_clauses : theory -> thm list -> hol_clause list
    9.11 +  val make_axiom_clauses :
    9.12 +    theory -> (thm * (axiom_name * hol_clause_id)) list
    9.13 +    -> (axiom_name * hol_clause) list
    9.14    val type_wrapper_name : string
    9.15    val get_helper_clauses :
    9.16 -    bool -> theory -> bool -> bool -> hol_clause list
    9.17 -      -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
    9.18 +    theory -> bool -> bool -> hol_clause list
    9.19 +    -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
    9.20    val write_tptp_file : bool -> bool -> bool -> Path.T ->
    9.21      hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    9.22      classrel_clause list * arity_clause list -> name_pool option * int
    9.23 -  val write_dfg_file : bool -> bool -> Path.T ->
    9.24 -    hol_clause list * hol_clause list * hol_clause list * hol_clause list *
    9.25 -    classrel_clause list * arity_clause list -> name_pool option * int
    9.26  end
    9.27  
    9.28  structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE =
    9.29 @@ -98,65 +96,66 @@
    9.30  
    9.31  fun isTaut (HOLClause {literals,...}) = exists isTrue literals;
    9.32  
    9.33 -fun type_of dfg (Type (a, Ts)) =
    9.34 -    let val (folTypes,ts) = types_of dfg Ts in
    9.35 -      (TyConstr (`(make_fixed_type_const dfg) a, folTypes), ts)
    9.36 +fun type_of (Type (a, Ts)) =
    9.37 +    let val (folTypes,ts) = types_of Ts in
    9.38 +      (TyConstr (`make_fixed_type_const a, folTypes), ts)
    9.39      end
    9.40 -  | type_of _ (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
    9.41 -  | type_of _ (tp as TVar (x, _)) =
    9.42 +  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
    9.43 +  | type_of (tp as TVar (x, _)) =
    9.44      (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
    9.45 -and types_of dfg Ts =
    9.46 -      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    9.47 -      in  (folTyps, union_all ts)  end;
    9.48 +and types_of Ts =
    9.49 +    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
    9.50 +      (folTyps, union_all ts)
    9.51 +    end
    9.52  
    9.53  (* same as above, but no gathering of sort information *)
    9.54 -fun simp_type_of dfg (Type (a, Ts)) =
    9.55 -      TyConstr (`(make_fixed_type_const dfg) a, map (simp_type_of dfg) Ts)
    9.56 -  | simp_type_of _ (TFree (a, _)) = TyFree (`make_fixed_type_var a)
    9.57 -  | simp_type_of _ (TVar (x, _)) =
    9.58 -    TyVar (make_schematic_type_var x, string_of_indexname x);
    9.59 +fun simp_type_of (Type (a, Ts)) =
    9.60 +      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
    9.61 +  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
    9.62 +  | simp_type_of (TVar (x, _)) =
    9.63 +    TyVar (make_schematic_type_var x, string_of_indexname x)
    9.64  
    9.65  
    9.66  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
    9.67 -fun combterm_of dfg thy (Const (c, T)) =
    9.68 +fun combterm_of thy (Const (c, T)) =
    9.69        let
    9.70 -        val (tp, ts) = type_of dfg T
    9.71 +        val (tp, ts) = type_of T
    9.72          val tvar_list =
    9.73            (if String.isPrefix skolem_theory_name c then
    9.74               [] |> Term.add_tvarsT T |> map TVar
    9.75             else
    9.76               (c, T) |> Sign.const_typargs thy)
    9.77 -          |> map (simp_type_of dfg)
    9.78 -        val c' = CombConst (`(make_fixed_const dfg) c, tp, tvar_list)
    9.79 +          |> map simp_type_of
    9.80 +        val c' = CombConst (`make_fixed_const c, tp, tvar_list)
    9.81        in  (c',ts)  end
    9.82 -  | combterm_of dfg _ (Free(v, T)) =
    9.83 -      let val (tp,ts) = type_of dfg T
    9.84 +  | combterm_of _ (Free(v, T)) =
    9.85 +      let val (tp,ts) = type_of T
    9.86            val v' = CombConst (`make_fixed_var v, tp, [])
    9.87        in  (v',ts)  end
    9.88 -  | combterm_of dfg _ (Var(v, T)) =
    9.89 -      let val (tp,ts) = type_of dfg T
    9.90 +  | combterm_of _ (Var(v, T)) =
    9.91 +      let val (tp,ts) = type_of T
    9.92            val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
    9.93        in  (v',ts)  end
    9.94 -  | combterm_of dfg thy (P $ Q) =
    9.95 -      let val (P',tsP) = combterm_of dfg thy P
    9.96 -          val (Q',tsQ) = combterm_of dfg thy Q
    9.97 -      in  (CombApp(P',Q'), union (op =) tsP tsQ)  end
    9.98 -  | combterm_of _ _ (t as Abs _) = raise CLAUSE ("HOL clause", t);
    9.99 -
   9.100 -fun predicate_of dfg thy ((@{const Not} $ P), polarity) = predicate_of dfg thy (P, not polarity)
   9.101 -  | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
   9.102 +  | combterm_of thy (P $ Q) =
   9.103 +      let val (P', tsP) = combterm_of thy P
   9.104 +          val (Q', tsQ) = combterm_of thy Q
   9.105 +      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   9.106 +  | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
   9.107  
   9.108 -fun literals_of_term1 dfg thy args (@{const Trueprop} $ P) = literals_of_term1 dfg thy args P
   9.109 -  | literals_of_term1 dfg thy args (@{const "op |"} $ P $ Q) =
   9.110 -      literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
   9.111 -  | literals_of_term1 dfg thy (lits,ts) P =
   9.112 -      let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
   9.113 -      in
   9.114 -          (Literal(pol,pred)::lits, union (op =) ts ts')
   9.115 -      end;
   9.116 +fun predicate_of thy ((@{const Not} $ P), polarity) =
   9.117 +    predicate_of thy (P, not polarity)
   9.118 +  | predicate_of thy (t, polarity) =
   9.119 +    (combterm_of thy (Envir.eta_contract t), polarity)
   9.120  
   9.121 -fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
   9.122 -val literals_of_term = literals_of_term_dfg false;
   9.123 +fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   9.124 +    literals_of_term1 args thy P
   9.125 +  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
   9.126 +    literals_of_term1 (literals_of_term1 args thy P) thy Q
   9.127 +  | literals_of_term1 (lits, ts) thy P =
   9.128 +    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   9.129 +      (Literal (pol, pred) :: lits, union (op =) ts ts')
   9.130 +    end
   9.131 +val literals_of_term = literals_of_term1 ([], [])
   9.132  
   9.133  fun skolem_name i j num_T_args =
   9.134    skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   9.135 @@ -199,11 +198,11 @@
   9.136  exception TRIVIAL;
   9.137  
   9.138  (* making axiom and conjecture clauses *)
   9.139 -fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
   9.140 +fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
   9.141    let
   9.142      val (skolem_somes, t) =
   9.143        th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
   9.144 -    val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
   9.145 +    val (lits, ctypes_sorts) = literals_of_term thy t
   9.146    in
   9.147      if forall isFalse lits then
   9.148        raise TRIVIAL
   9.149 @@ -213,29 +212,26 @@
   9.150                    kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   9.151    end
   9.152  
   9.153 -fun add_axiom_clause dfg thy (th, (name, id)) (skolem_somes, clss) =
   9.154 +fun add_axiom_clause thy (th, (name, id)) (skolem_somes, clss) =
   9.155    let
   9.156 -    val (skolem_somes, cls) =
   9.157 -      make_clause dfg thy (id, name, Axiom, th) skolem_somes
   9.158 +    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
   9.159    in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
   9.160  
   9.161 -fun make_axiom_clauses dfg thy clauses =
   9.162 -  ([], []) |> fold (add_axiom_clause dfg thy) clauses |> snd
   9.163 +fun make_axiom_clauses thy clauses =
   9.164 +  ([], []) |> fold (add_axiom_clause thy) clauses |> snd
   9.165  
   9.166 -fun make_conjecture_clauses dfg thy =
   9.167 +fun make_conjecture_clauses thy =
   9.168    let
   9.169      fun aux _ _ [] = []
   9.170        | aux n skolem_somes (th :: ths) =
   9.171          let
   9.172            val (skolem_somes, cls) =
   9.173 -            make_clause dfg thy (n, "conjecture", Conjecture, th) skolem_somes
   9.174 +            make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
   9.175          in cls :: aux (n + 1) skolem_somes ths end
   9.176    in aux 0 [] end
   9.177  
   9.178  (**********************************************************************)
   9.179 -(* convert clause into ATP specific formats:                          *)
   9.180 -(* TPTP used by Vampire and E                                         *)
   9.181 -(* DFG used by SPASS                                                  *)
   9.182 +(* convert clause into TPTP format                                    *)
   9.183  (**********************************************************************)
   9.184  
   9.185  (*Result of a function type; no need to check that the argument type matches.*)
   9.186 @@ -315,17 +311,11 @@
   9.187    string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
   9.188  
   9.189  fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
   9.190 -  case t of
   9.191 -    (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
   9.192 -    (* DFG only: new TPTP prefers infix equality *)
   9.193 -    pool_map (string_of_combterm params) [t1, t2]
   9.194 -    #>> prefix "equal" o paren_pack
   9.195 -  | _ =>
   9.196 -    case #1 (strip_combterm_comb t) of
   9.197 -      CombConst ((s, _), _, _) =>
   9.198 -      (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   9.199 -          params t
   9.200 -    | _ => boolify params t
   9.201 +  case #1 (strip_combterm_comb t) of
   9.202 +    CombConst ((s, _), _, _) =>
   9.203 +    (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
   9.204 +        params t
   9.205 +  | _ => boolify params t
   9.206  
   9.207  
   9.208  (*** TPTP format ***)
   9.209 @@ -353,7 +343,7 @@
   9.210  
   9.211  fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
   9.212                  pool =
   9.213 -let
   9.214 +  let
   9.215      val ((lits, tylits), pool) =
   9.216        tptp_type_literals params (kind = Conjecture) cls pool
   9.217    in
   9.218 @@ -361,94 +351,6 @@
   9.219    end
   9.220  
   9.221  
   9.222 -(*** DFG format ***)
   9.223 -
   9.224 -fun dfg_literal params (Literal (pos, pred)) =
   9.225 -  string_of_predicate params pred #>> dfg_sign pos
   9.226 -
   9.227 -fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
   9.228 -  pool_map (dfg_literal params) literals
   9.229 -  #>> rpair (map (dfg_of_type_literal pos)
   9.230 -                 (type_literals_for_types ctypes_sorts))
   9.231 -
   9.232 -fun get_uvars (CombConst _) vars pool = (vars, pool)
   9.233 -  | get_uvars (CombVar (name, _)) vars pool =
   9.234 -    nice_name name pool |>> (fn var => var :: vars)
   9.235 -  | get_uvars (CombApp (P, Q)) vars pool =
   9.236 -    let val (vars, pool) = get_uvars P vars pool in get_uvars Q vars pool end
   9.237 -
   9.238 -fun get_uvars_l (Literal (_, c)) = get_uvars c [];
   9.239 -
   9.240 -fun dfg_vars (HOLClause {literals, ...}) =
   9.241 -  pool_map get_uvars_l literals #>> union_all
   9.242 -
   9.243 -fun dfg_clause params (cls as HOLClause {axiom_name, clause_id, kind,
   9.244 -                                         ctypes_sorts, ...}) pool =
   9.245 -  let
   9.246 -    val ((lits, tylits), pool) =
   9.247 -      dfg_type_literals params (kind = Conjecture) cls pool
   9.248 -    val (vars, pool) = dfg_vars cls pool
   9.249 -    val tvars = get_tvar_strs ctypes_sorts
   9.250 -  in
   9.251 -    ((gen_dfg_cls (clause_id, axiom_name, kind, lits, tylits, tvars @ vars),
   9.252 -      tylits), pool)
   9.253 -  end
   9.254 -
   9.255 -
   9.256 -(** For DFG format: accumulate function and predicate declarations **)
   9.257 -
   9.258 -fun add_types tvars = fold add_fol_type_funcs tvars
   9.259 -
   9.260 -fun add_decls (full_types, explicit_apply, cma, cnh)
   9.261 -              (CombConst ((c, _), ctp, tvars)) (funcs, preds) =
   9.262 -      (if c = "equal" then
   9.263 -         (add_types tvars funcs, preds)
   9.264 -       else
   9.265 -         let val arity = min_arity_of cma c
   9.266 -             val ntys = if not full_types then length tvars else 0
   9.267 -             val addit = Symtab.update(c, arity + ntys)
   9.268 -         in
   9.269 -             if needs_hBOOL explicit_apply cnh c then
   9.270 -               (add_types tvars (addit funcs), preds)
   9.271 -             else
   9.272 -               (add_types tvars funcs, addit preds)
   9.273 -         end) |>> full_types ? add_fol_type_funcs ctp
   9.274 -  | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
   9.275 -      (add_fol_type_funcs ctp funcs, preds)
   9.276 -  | add_decls params (CombApp (P, Q)) decls =
   9.277 -      decls |> add_decls params P |> add_decls params Q
   9.278 -
   9.279 -fun add_literal_decls params (Literal (_, c)) = add_decls params c
   9.280 -
   9.281 -fun add_clause_decls params (HOLClause {literals, ...}) decls =
   9.282 -    fold (add_literal_decls params) literals decls
   9.283 -    handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   9.284 -
   9.285 -fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses
   9.286 -                     arity_clauses =
   9.287 -  let
   9.288 -    val functab =
   9.289 -      init_functab
   9.290 -      |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
   9.291 -                             ("tc_bool", 0)]
   9.292 -      val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
   9.293 -      val (functab, predtab) =
   9.294 -        (functab, predtab) |> fold (add_clause_decls params) clauses
   9.295 -                           |>> fold add_arity_clause_funcs arity_clauses
   9.296 -  in (Symtab.dest functab, Symtab.dest predtab) end
   9.297 -
   9.298 -fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds =
   9.299 -  fold add_type_sort_preds ctypes_sorts preds
   9.300 -  handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
   9.301 -
   9.302 -(*Higher-order clauses have only the predicates hBOOL and type classes.*)
   9.303 -fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   9.304 -  Symtab.empty
   9.305 -  |> fold add_clause_preds clauses
   9.306 -  |> fold add_arity_clause_preds arity_clauses
   9.307 -  |> fold add_classrel_clause_preds clsrel_clauses
   9.308 -  |> Symtab.dest
   9.309 -
   9.310  (**********************************************************************)
   9.311  (* write clauses to files                                             *)
   9.312  (**********************************************************************)
   9.313 @@ -480,9 +382,9 @@
   9.314    Symtab.make (maps (maps (map (rpair 0) o fst))
   9.315                      [optional_helpers, optional_typed_helpers])
   9.316  
   9.317 -fun get_helper_clauses dfg thy is_FO full_types conjectures axcls =
   9.318 +fun get_helper_clauses thy is_FO full_types conjectures axcls =
   9.319    let
   9.320 -    val axclauses = map snd (make_axiom_clauses dfg thy axcls)
   9.321 +    val axclauses = map snd (make_axiom_clauses thy axcls)
   9.322      val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
   9.323      fun is_needed c = the (Symtab.lookup ct c) > 0
   9.324      val cnfs =
   9.325 @@ -492,7 +394,7 @@
   9.326                     if exists is_needed ss then cnf_helper_thms thy raw ths
   9.327                     else []))
   9.328        @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   9.329 -  in map snd (make_axiom_clauses dfg thy cnfs) end
   9.330 +  in map snd (make_axiom_clauses thy cnfs) end
   9.331  
   9.332  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   9.333    are not at top level, to see if hBOOL is needed.*)
   9.334 @@ -521,7 +423,7 @@
   9.335                             (const_min_arity, const_needs_hBOOL) =
   9.336    fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
   9.337  
   9.338 -fun display_arity explicit_apply const_needs_hBOOL (c,n) =
   9.339 +fun display_arity explicit_apply const_needs_hBOOL (c, n) =
   9.340    trace_msg (fn () => "Constant: " ^ c ^
   9.341                  " arity:\t" ^ Int.toString n ^
   9.342                  (if needs_hBOOL explicit_apply const_needs_hBOOL c then
   9.343 @@ -541,10 +443,6 @@
   9.344       in (const_min_arity, const_needs_hBOOL) end
   9.345    else (Symtab.empty, Symtab.empty);
   9.346  
   9.347 -fun header () =
   9.348 -  "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^
   9.349 -  "% " ^ timestamp () ^ "\n"
   9.350 -
   9.351  (* TPTP format *)
   9.352  
   9.353  fun write_tptp_file readable_names full_types explicit_apply file clauses =
   9.354 @@ -572,7 +470,8 @@
   9.355        + length helper_clss
   9.356      val _ =
   9.357        File.write_list file
   9.358 -          (header () ::
   9.359 +          ("% This file was generated by Isabelle (most likely Sledgehammer)\n\
   9.360 +           \% " ^ timestamp () ^ "\n" ::
   9.361             section "Relevant fact" ax_clss @
   9.362             section "Class relationship" classrel_clss @
   9.363             section "Arity declaration" arity_clss @
   9.364 @@ -581,53 +480,4 @@
   9.365             section "Type variable" tfree_clss)
   9.366    in (pool, conjecture_offset) end
   9.367  
   9.368 -(* DFG format *)
   9.369 -
   9.370 -fun dfg_tfree_predicate s = (first_field "(" s |> the |> fst, 1)
   9.371 -
   9.372 -fun write_dfg_file full_types explicit_apply file clauses =
   9.373 -  let
   9.374 -    (* Some of the helper functions below are not name-pool-aware. However,
   9.375 -       there's no point in adding name pool support if the DFG format is on its
   9.376 -       way out anyway. *)
   9.377 -    val pool = NONE
   9.378 -    val (conjectures, axclauses, _, helper_clauses,
   9.379 -      classrel_clauses, arity_clauses) = clauses
   9.380 -    val (cma, cnh) = count_constants explicit_apply clauses
   9.381 -    val params = (full_types, explicit_apply, cma, cnh)
   9.382 -    val ((conjecture_clss, tfree_litss), pool) =
   9.383 -      pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
   9.384 -    val tfree_lits = union_all tfree_litss
   9.385 -    val problem_name = Path.implode (Path.base file)
   9.386 -    val (axstrs, pool) = pool_map (apfst fst oo dfg_clause params) axclauses pool
   9.387 -    val tfree_clss = map dfg_tfree_clause tfree_lits
   9.388 -    val tfree_preds = map dfg_tfree_predicate tfree_lits
   9.389 -    val (helper_clauses_strs, pool) =
   9.390 -      pool_map (apfst fst oo dfg_clause params) helper_clauses pool
   9.391 -    val (funcs, cl_preds) =
   9.392 -      decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   9.393 -    val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   9.394 -    val preds = tfree_preds @ cl_preds @ ty_preds
   9.395 -    val conjecture_offset =
   9.396 -      length axclauses + length classrel_clauses + length arity_clauses
   9.397 -      + length helper_clauses
   9.398 -    val _ =
   9.399 -      File.write_list file
   9.400 -          (header () ::
   9.401 -           string_of_start problem_name ::
   9.402 -           string_of_descrip problem_name ::
   9.403 -           string_of_symbols (string_of_funcs funcs)
   9.404 -                             (string_of_preds preds) ::
   9.405 -           "list_of_clauses(axioms, cnf).\n" ::
   9.406 -           axstrs @
   9.407 -           map dfg_classrel_clause classrel_clauses @
   9.408 -           map dfg_arity_clause arity_clauses @
   9.409 -           helper_clauses_strs @
   9.410 -           ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @
   9.411 -           conjecture_clss @
   9.412 -           tfree_clss @
   9.413 -           ["end_of_list.\n\n",
   9.414 -            "end_problem.\n"])
   9.415 -  in (pool, conjecture_offset) end
   9.416 -
   9.417  end;
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 22 13:17:59 2010 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 22 14:28:22 2010 +0200
    10.3 @@ -58,7 +58,6 @@
    10.4    {add = [], del = ns, only = false}
    10.5  fun only_relevance_override ns : relevance_override =
    10.6    {add = ns, del = [], only = true}
    10.7 -val no_relevance_override = add_to_relevance_override []
    10.8  fun merge_relevance_override_pairwise (r1 : relevance_override)
    10.9                                        (r2 : relevance_override) =
   10.10    {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
   10.11 @@ -166,7 +165,7 @@
   10.12  val infinity_time_in_secs = 60 * 60 * 24 * 365
   10.13  val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
   10.14  
   10.15 -fun extract_params thy default_params override_params =
   10.16 +fun extract_params default_params override_params =
   10.17    let
   10.18      val override_params = map unalias_raw_param override_params
   10.19      val raw_params = rev override_params @ rev default_params
   10.20 @@ -216,7 +215,7 @@
   10.21       timeout = timeout, minimize_timeout = minimize_timeout}
   10.22    end
   10.23  
   10.24 -fun get_params thy = extract_params thy (default_raw_params thy)
   10.25 +fun get_params thy = extract_params (default_raw_params thy)
   10.26  fun default_params thy = get_params thy o map (apsnd single)
   10.27  
   10.28  val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
   10.29 @@ -264,7 +263,6 @@
   10.30  val running_atpsN = "running_atps"
   10.31  val kill_atpsN = "kill_atps"
   10.32  val refresh_tptpN = "refresh_tptp"
   10.33 -val helpN = "help"
   10.34  
   10.35  fun minimizize_raw_param_name "timeout" = "minimize_timeout"
   10.36    | minimizize_raw_param_name name = name
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jun 22 13:17:59 2010 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jun 22 14:28:22 2010 +0200
    11.3 @@ -368,7 +368,7 @@
    11.4    | add_type_constraint _ = I
    11.5  
    11.6  fun is_positive_literal (@{const Not} $ _) = false
    11.7 -  | is_positive_literal t = true
    11.8 +  | is_positive_literal _ = true
    11.9  
   11.10  fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   11.11      Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
   11.12 @@ -551,11 +551,11 @@
   11.13  (* Vampire is keen on producing these. *)
   11.14  fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
   11.15                                          $ t1 $ t2)) = (t1 aconv t2)
   11.16 -  | is_trivial_formula t = false
   11.17 +  | is_trivial_formula _ = false
   11.18  
   11.19 -fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
   11.20 +fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
   11.21      (j, line :: map (replace_deps_in_line (num, [])) lines)
   11.22 -  | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
   11.23 +  | add_desired_line isar_shrink_factor conjecture_shape thm_names frees
   11.24                       (Inference (num, t, deps)) (j, lines) =
   11.25      (j + 1,
   11.26       if is_axiom_clause_number thm_names num orelse
   11.27 @@ -667,7 +667,7 @@
   11.28  
   11.29  fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
   11.30  
   11.31 -fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
   11.32 +fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   11.33    | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
   11.34    | step_for_line thm_names j (Inference (num, t, deps)) =
   11.35      Have (if j = 1 then [Show] else [], (raw_prefix, num),
   11.36 @@ -683,7 +683,7 @@
   11.37        |> decode_lines ctxt full_types tfrees
   11.38        |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
   11.39        |> rpair [] |-> fold_rev add_nontrivial_line
   11.40 -      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
   11.41 +      |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   11.42                                                 conjecture_shape thm_names frees)
   11.43        |> snd
   11.44    in
   11.45 @@ -722,7 +722,7 @@
   11.46          else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   11.47            aux (hd proof1 :: proof_tail) (map tl proofs)
   11.48          else case hd proof1 of
   11.49 -          Have ([], l, t, by) =>
   11.50 +          Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   11.51            if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   11.52                        | _ => false) (tl proofs) andalso
   11.53               not (exists (member (op =) (maps new_labels_of proofs))
   11.54 @@ -755,7 +755,7 @@
   11.55          first_pass (proof, contra) |>> cons step
   11.56        | first_pass ((step as Let _) :: proof, contra) =
   11.57          first_pass (proof, contra) |>> cons step
   11.58 -      | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
   11.59 +      | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
   11.60          if member (op =) concl_ls l then
   11.61            first_pass (proof, contra ||> l = hd concl_ls ? cons step)
   11.62          else
   11.63 @@ -992,6 +992,13 @@
   11.64          do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   11.65    in do_proof end
   11.66  
   11.67 +fun strip_subgoal goal i =
   11.68 +  let
   11.69 +    val (t, frees) = Logic.goal_params (prop_of goal) i
   11.70 +    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
   11.71 +    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
   11.72 +  in (rev (map dest_Free frees), hyp_ts, concl_t) end
   11.73 +
   11.74  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   11.75                      (other_params as (full_types, _, atp_proof, thm_names, goal,
   11.76                                        i)) =
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 22 13:17:59 2010 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 22 14:28:22 2010 +0200
    12.3 @@ -6,7 +6,6 @@
    12.4  
    12.5  signature SLEDGEHAMMER_UTIL =
    12.6  sig
    12.7 -  val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
    12.8    val plural_s : int -> string
    12.9    val serial_commas : string -> string list -> string list
   12.10    val replace_all : string -> string -> string -> string
   12.11 @@ -24,8 +23,6 @@
   12.12  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
   12.13  struct
   12.14  
   12.15 -fun pairf f g x = (f x, g x)
   12.16 -
   12.17  fun plural_s n = if n = 1 then "" else "s"
   12.18  
   12.19  fun serial_commas _ [] = ["??"]