implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
authorblanchet
Wed Dec 15 11:26:28 2010 +0100 (2010-12-15)
changeset 4113630bedf58b177
parent 41135 8c5d44c7e8af
child 41137 8b634031b2a5
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -9,10 +9,11 @@
     1.4  signature SLEDGEHAMMER_ATP_RECONSTRUCT =
     1.5  sig
     1.6    type locality = Sledgehammer_Filter.locality
     1.7 +  type type_system = Sledgehammer_ATP_Translate.type_system
     1.8    type minimize_command = string list -> string
     1.9    type metis_params =
    1.10 -    string * bool * minimize_command * string * (string * locality) list vector
    1.11 -    * thm * int
    1.12 +    string * type_system * minimize_command * string
    1.13 +    * (string * locality) list vector * thm * int
    1.14    type isar_params =
    1.15      string Symtab.table * bool * int * Proof.context * int list list
    1.16    type text_result = string * (string * locality) list
    1.17 @@ -43,8 +44,8 @@
    1.18  
    1.19  type minimize_command = string list -> string
    1.20  type metis_params =
    1.21 -  string * bool * minimize_command * string * (string * locality) list vector
    1.22 -  * thm * int
    1.23 +  string * type_system * minimize_command * string
    1.24 +  * (string * locality) list vector * thm * int
    1.25  type isar_params =
    1.26    string Symtab.table * bool * int * Proof.context * int list list
    1.27  type text_result = string * (string * locality) list
    1.28 @@ -125,12 +126,12 @@
    1.29  fun using_labels [] = ""
    1.30    | using_labels ls =
    1.31      "using " ^ space_implode " " (map string_for_label ls) ^ " "
    1.32 -fun metis_name full_types = if full_types then "metisFT" else "metis"
    1.33 -fun metis_call full_types ss = command_call (metis_name full_types) ss
    1.34 -fun metis_command full_types i n (ls, ss) =
    1.35 -  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
    1.36 -fun metis_line banner full_types i n ss =
    1.37 -  try_command_line banner (metis_command full_types i n ([], ss))
    1.38 +fun metis_name type_sys = if is_fully_typed type_sys then "metisFT" else "metis"
    1.39 +fun metis_call type_sys ss = command_call (metis_name type_sys) ss
    1.40 +fun metis_command type_sys i n (ls, ss) =
    1.41 +  using_labels ls ^ apply_on_subgoal i n ^ metis_call type_sys ss
    1.42 +fun metis_line banner type_sys i n ss =
    1.43 +  try_command_line banner (metis_command type_sys i n ([], ss))
    1.44  fun minimize_line _ [] = ""
    1.45    | minimize_line minimize_command ss =
    1.46      case minimize_command ss of
    1.47 @@ -165,14 +166,14 @@
    1.48    List.partition (curry (op =) Chained o snd)
    1.49    #> pairself (sort_distinct (string_ord o pairself fst))
    1.50  
    1.51 -fun metis_proof_text (banner, full_types, minimize_command,
    1.52 -                      tstplike_proof, fact_names, goal, i) =
    1.53 +fun metis_proof_text (banner, type_sys, minimize_command, tstplike_proof,
    1.54 +                      fact_names, goal, i) =
    1.55    let
    1.56      val (chained_lemmas, other_lemmas) =
    1.57        split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
    1.58      val n = Logic.count_prems (prop_of goal)
    1.59    in
    1.60 -    (metis_line banner full_types i n (map fst other_lemmas) ^
    1.61 +    (metis_line banner type_sys i n (map fst other_lemmas) ^
    1.62       minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
    1.63       other_lemmas @ chained_lemmas)
    1.64    end
    1.65 @@ -303,7 +304,7 @@
    1.66  
    1.67  (* First-order translation. No types are known for variables. "HOLogic.typeT"
    1.68     should allow them to be inferred. *)
    1.69 -fun raw_term_from_pred thy full_types tfrees =
    1.70 +fun raw_term_from_pred thy type_sys tfrees =
    1.71    let
    1.72      fun aux opt_T extra_us u =
    1.73        case u of
    1.74 @@ -327,25 +328,26 @@
    1.75          | SOME b =>
    1.76            let
    1.77              val c = invert_const b
    1.78 -            val num_type_args = num_type_args thy c
    1.79 -            val (type_us, term_us) =
    1.80 -              chop (if full_types then 0 else num_type_args) us
    1.81 +            val num_ty_args = num_atp_type_args thy type_sys c
    1.82 +            val (type_us, term_us) = chop num_ty_args us
    1.83              (* Extra args from "hAPP" come after any arguments given directly to
    1.84                 the constant. *)
    1.85              val term_ts = map (aux NONE []) term_us
    1.86              val extra_ts = map (aux NONE []) extra_us
    1.87              val t =
    1.88 -              Const (c, if full_types then
    1.89 +              Const (c, if is_fully_typed type_sys then
    1.90                            case opt_T of
    1.91                              SOME T => map fastype_of term_ts ---> T
    1.92                            | NONE =>
    1.93 -                            if num_type_args = 0 then
    1.94 +                            if num_type_args thy c = 0 then
    1.95                                Sign.const_instance thy (c, [])
    1.96                              else
    1.97                                raise Fail ("no type information for " ^ quote c)
    1.98 -                        else
    1.99 +                        else if num_type_args thy c = length type_us then
   1.100                            Sign.const_instance thy (c,
   1.101 -                              map (type_from_fo_term tfrees) type_us))
   1.102 +                              map (type_from_fo_term tfrees) type_us)
   1.103 +                        else
   1.104 +                          HOLogic.typeT)
   1.105            in list_comb (t, term_ts @ extra_ts) end
   1.106          | NONE => (* a free or schematic variable *)
   1.107            let
   1.108 @@ -366,12 +368,12 @@
   1.109            in list_comb (t, ts) end
   1.110    in aux (SOME HOLogic.boolT) [] end
   1.111  
   1.112 -fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
   1.113 +fun term_from_pred thy type_sys tfrees pos (u as ATerm (s, _)) =
   1.114    if String.isPrefix class_prefix s then
   1.115      add_type_constraint (type_constraint_from_term pos tfrees u)
   1.116      #> pair @{const True}
   1.117    else
   1.118 -    pair (raw_term_from_pred thy full_types tfrees u)
   1.119 +    pair (raw_term_from_pred thy type_sys tfrees u)
   1.120  
   1.121  val combinator_table =
   1.122    [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
   1.123 @@ -412,7 +414,7 @@
   1.124  
   1.125  (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   1.126     appear in the formula. *)
   1.127 -fun prop_from_formula thy full_types tfrees phi =
   1.128 +fun prop_from_formula thy type_sys tfrees phi =
   1.129    let
   1.130      fun do_formula pos phi =
   1.131        case phi of
   1.132 @@ -435,7 +437,7 @@
   1.133               | AIff => s_iff
   1.134               | ANotIff => s_not o s_iff
   1.135               | _ => raise Fail "unexpected connective")
   1.136 -      | AAtom tm => term_from_pred thy full_types tfrees pos tm
   1.137 +      | AAtom tm => term_from_pred thy type_sys tfrees pos tm
   1.138        | _ => raise FORMULA [phi]
   1.139    in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   1.140  
   1.141 @@ -449,14 +451,14 @@
   1.142  fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   1.143    | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   1.144  
   1.145 -fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
   1.146 +fun decode_line type_sys tfrees (Definition (name, phi1, phi2)) ctxt =
   1.147      let
   1.148        val thy = ProofContext.theory_of ctxt
   1.149 -      val t1 = prop_from_formula thy full_types tfrees phi1
   1.150 +      val t1 = prop_from_formula thy type_sys tfrees phi1
   1.151        val vars = snd (strip_comb t1)
   1.152        val frees = map unvarify_term vars
   1.153        val unvarify_args = subst_atomic (vars ~~ frees)
   1.154 -      val t2 = prop_from_formula thy full_types tfrees phi2
   1.155 +      val t2 = prop_from_formula thy type_sys tfrees phi2
   1.156        val (t1, t2) =
   1.157          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   1.158          |> unvarify_args |> uncombine_term |> check_formula ctxt
   1.159 @@ -465,17 +467,17 @@
   1.160        (Definition (name, t1, t2),
   1.161         fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   1.162      end
   1.163 -  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   1.164 +  | decode_line type_sys tfrees (Inference (name, u, deps)) ctxt =
   1.165      let
   1.166        val thy = ProofContext.theory_of ctxt
   1.167 -      val t = u |> prop_from_formula thy full_types tfrees
   1.168 +      val t = u |> prop_from_formula thy type_sys tfrees
   1.169                  |> uncombine_term |> check_formula ctxt
   1.170      in
   1.171        (Inference (name, t, deps),
   1.172         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   1.173      end
   1.174 -fun decode_lines ctxt full_types tfrees lines =
   1.175 -  fst (fold_map (decode_line full_types tfrees) lines ctxt)
   1.176 +fun decode_lines ctxt type_sys tfrees lines =
   1.177 +  fst (fold_map (decode_line type_sys tfrees) lines ctxt)
   1.178  
   1.179  fun is_same_inference _ (Definition _) = false
   1.180    | is_same_inference t (Inference (_, t', _)) = t aconv t'
   1.181 @@ -605,16 +607,15 @@
   1.182      else
   1.183        s
   1.184  
   1.185 -fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   1.186 -        isar_shrink_factor tstplike_proof conjecture_shape fact_names params
   1.187 -        frees =
   1.188 +fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor
   1.189 +        tstplike_proof conjecture_shape fact_names params frees =
   1.190    let
   1.191      val lines =
   1.192        tstplike_proof
   1.193        |> atp_proof_from_tstplike_string
   1.194        |> nasty_atp_proof pool
   1.195        |> map_term_names_in_atp_proof repair_name
   1.196 -      |> decode_lines ctxt full_types tfrees
   1.197 +      |> decode_lines ctxt type_sys tfrees
   1.198        |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
   1.199        |> rpair [] |-> fold_rev add_nontrivial_line
   1.200        |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   1.201 @@ -857,7 +858,7 @@
   1.202          step :: aux subst depth nextp proof
   1.203    in aux [] 0 (1, 1) end
   1.204  
   1.205 -fun string_for_proof ctxt0 full_types i n =
   1.206 +fun string_for_proof ctxt0 type_sys i n =
   1.207    let
   1.208      val ctxt = ctxt0
   1.209        |> Config.put show_free_types false
   1.210 @@ -879,7 +880,7 @@
   1.211           if member (op =) qs Show then "show" else "have")
   1.212      val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   1.213      fun do_facts (ls, ss) =
   1.214 -      metis_command full_types 1 1
   1.215 +      metis_command type_sys 1 1
   1.216                      (ls |> sort_distinct (prod_ord string_ord int_ord),
   1.217                       ss |> sort_distinct string_ord)
   1.218      and do_step ind (Fix xs) =
   1.219 @@ -914,7 +915,7 @@
   1.220    in do_proof end
   1.221  
   1.222  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   1.223 -                    (metis_params as (_, full_types, _, tstplike_proof,
   1.224 +                    (metis_params as (_, type_sys, _, tstplike_proof,
   1.225                                        fact_names, goal, i)) =
   1.226    let
   1.227      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   1.228 @@ -923,7 +924,7 @@
   1.229      val n = Logic.count_prems (prop_of goal)
   1.230      val (one_line_proof, lemma_names) = metis_proof_text metis_params
   1.231      fun isar_proof_for () =
   1.232 -      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   1.233 +      case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees
   1.234                 isar_shrink_factor tstplike_proof conjecture_shape fact_names
   1.235                 params frees
   1.236             |> redirect_proof hyp_ts concl_t
   1.237 @@ -931,7 +932,7 @@
   1.238             |> then_chain_proof
   1.239             |> kill_useless_labels_in_proof
   1.240             |> relabel_proof
   1.241 -           |> string_for_proof ctxt full_types i n of
   1.242 +           |> string_for_proof ctxt type_sys i n of
   1.243          "" => "\nNo structured proof available."
   1.244        | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   1.245      val isar_proof =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
     2.3 @@ -20,6 +20,8 @@
     2.4  
     2.5    val fact_prefix : string
     2.6    val conjecture_prefix : string
     2.7 +  val is_fully_typed : type_system -> bool
     2.8 +  val num_atp_type_args : theory -> type_system -> string -> int
     2.9    val translate_atp_fact :
    2.10      Proof.context -> (string * 'a) * thm
    2.11      -> translated_formula option * ((string * 'a) * thm)
    2.12 @@ -63,6 +65,24 @@
    2.13    | is_fully_typed (Preds full_types) = full_types
    2.14    | is_fully_typed _ = false
    2.15  
    2.16 +(* This is an approximation. If it returns "true" for a constant that isn't
    2.17 +   overloaded (i.e., that has one uniform definition), needless clutter is
    2.18 +   generated; if it returns "false" for an overloaded constant, the ATP gets a
    2.19 +   license to do unsound reasoning if the type system is "overloaded_args". *)
    2.20 +fun is_overloaded thy s =
    2.21 +  length (Defs.specifications_of (Theory.defs_of thy) s) > 1
    2.22 +
    2.23 +fun needs_type_args thy type_sys s =
    2.24 +  case type_sys of
    2.25 +    Tags full_types => not full_types
    2.26 +  | Preds full_types => not full_types
    2.27 +  | Const_Args => true
    2.28 +  | Overload_Args => is_overloaded thy s
    2.29 +  | No_Types => false
    2.30 +
    2.31 +fun num_atp_type_args thy type_sys s =
    2.32 +  if needs_type_args thy type_sys s then num_type_args thy s else 0
    2.33 +
    2.34  fun mk_anot phi = AConn (ANot, [phi])
    2.35  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    2.36  fun mk_ahorn [] phi = phi
    2.37 @@ -308,7 +328,7 @@
    2.38  
    2.39  fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
    2.40  
    2.41 -fun fo_term_for_combterm type_sys =
    2.42 +fun fo_term_for_combterm thy type_sys =
    2.43    let
    2.44      fun aux top_level u =
    2.45        let
    2.46 @@ -316,18 +336,27 @@
    2.47          val (x, ty_args) =
    2.48            case head of
    2.49              CombConst (name as (s, s'), _, ty_args) =>
    2.50 -            let val ty_args = if is_fully_typed type_sys then [] else ty_args in
    2.51 -              if s = "equal" then
    2.52 -                if top_level andalso length args = 2 then (name, [])
    2.53 -                else (("c_fequal", @{const_name Metis.fequal}), ty_args)
    2.54 -              else if top_level then
    2.55 -                case s of
    2.56 -                  "c_False" => (("$false", s'), [])
    2.57 -                | "c_True" => (("$true", s'), [])
    2.58 -                | _ => (name, ty_args)
    2.59 -              else
    2.60 -                (name, ty_args)
    2.61 -            end
    2.62 +            (case strip_prefix_and_unascii const_prefix s of
    2.63 +               NONE =>
    2.64 +               if s = "equal" then
    2.65 +                 if top_level andalso length args = 2 then (name, [])
    2.66 +                 else (("c_fequal", @{const_name Metis.fequal}), ty_args)
    2.67 +               else
    2.68 +                 (name, ty_args)
    2.69 +             | SOME s'' =>
    2.70 +               let
    2.71 +                 val s'' = invert_const s''
    2.72 +                 val ty_args =
    2.73 +                   if needs_type_args thy type_sys s'' then ty_args else []
    2.74 +                in
    2.75 +                  if top_level then
    2.76 +                    case s of
    2.77 +                      "c_False" => (("$false", s'), [])
    2.78 +                    | "c_True" => (("$true", s'), [])
    2.79 +                    | _ => (name, ty_args)
    2.80 +                  else
    2.81 +                    (name, ty_args)
    2.82 +                end)
    2.83            | CombVar (name, _) => (name, [])
    2.84            | CombApp _ => raise Fail "impossible \"CombApp\""
    2.85          val t = ATerm (x, map fo_term_for_combtyp ty_args @
    2.86 @@ -340,21 +369,21 @@
    2.87      end
    2.88    in aux true end
    2.89  
    2.90 -fun formula_for_combformula type_sys =
    2.91 +fun formula_for_combformula thy type_sys =
    2.92    let
    2.93      fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
    2.94        | aux (AConn (c, phis)) = AConn (c, map aux phis)
    2.95 -      | aux (AAtom tm) = AAtom (fo_term_for_combterm type_sys tm)
    2.96 +      | aux (AAtom tm) = AAtom (fo_term_for_combterm thy type_sys tm)
    2.97    in aux end
    2.98  
    2.99 -fun formula_for_fact type_sys
   2.100 +fun formula_for_fact thy type_sys
   2.101                       ({combformula, ctypes_sorts, ...} : translated_formula) =
   2.102    mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   2.103                  (type_literals_for_types ctypes_sorts))
   2.104 -           (formula_for_combformula type_sys combformula)
   2.105 +           (formula_for_combformula thy type_sys combformula)
   2.106  
   2.107 -fun problem_line_for_fact prefix type_sys (formula as {name, kind, ...}) =
   2.108 -  Fof (prefix ^ ascii_of name, kind, formula_for_fact type_sys formula)
   2.109 +fun problem_line_for_fact thy prefix type_sys (formula as {name, kind, ...}) =
   2.110 +  Fof (prefix ^ ascii_of name, kind, formula_for_fact thy type_sys formula)
   2.111  
   2.112  fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   2.113                                                         superclass, ...}) =
   2.114 @@ -377,10 +406,10 @@
   2.115                  (formula_for_fo_literal
   2.116                       (fo_literal_for_arity_literal conclLit)))
   2.117  
   2.118 -fun problem_line_for_conjecture type_sys
   2.119 +fun problem_line_for_conjecture thy type_sys
   2.120          ({name, kind, combformula, ...} : translated_formula) =
   2.121    Fof (conjecture_prefix ^ name, kind,
   2.122 -       formula_for_combformula type_sys combformula)
   2.123 +       formula_for_combformula thy type_sys combformula)
   2.124  
   2.125  fun free_type_literals_for_conjecture
   2.126          ({ctypes_sorts, ...} : translated_formula) =
   2.127 @@ -427,10 +456,8 @@
   2.128          String.isPrefix type_const_prefix s orelse
   2.129          String.isPrefix class_prefix s then
   2.130         16383 (* large number *)
   2.131 -     else if is_fully_typed type_sys then
   2.132 -       0
   2.133       else case strip_prefix_and_unascii const_prefix s of
   2.134 -       SOME s' => num_type_args thy (invert_const s')
   2.135 +       SOME s' => num_atp_type_args thy type_sys (invert_const s')
   2.136       | NONE => 0)
   2.137    | min_arity_of _ _ (SOME the_const_tab) s =
   2.138      case Symtab.lookup the_const_tab s of
   2.139 @@ -528,11 +555,11 @@
   2.140      val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses,
   2.141                        arity_clauses)) =
   2.142        translate_formulas ctxt type_sys hyp_ts concl_t facts
   2.143 -    val fact_lines = map (problem_line_for_fact fact_prefix type_sys) facts
   2.144 +    val fact_lines = map (problem_line_for_fact thy fact_prefix type_sys) facts
   2.145      val helper_lines =
   2.146 -      map (problem_line_for_fact helper_prefix type_sys) helper_facts
   2.147 +      map (problem_line_for_fact thy helper_prefix type_sys) helper_facts
   2.148      val conjecture_lines =
   2.149 -      map (problem_line_for_conjecture type_sys) conjectures
   2.150 +      map (problem_line_for_conjecture thy type_sys) conjectures
   2.151      val tfree_lines = problem_lines_for_free_types conjectures
   2.152      val class_rel_lines =
   2.153        map problem_line_for_class_rel_clause class_rel_clauses
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:26:28 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:26:28 2010 +0100
     3.3 @@ -99,7 +99,7 @@
     3.4     ("no_isar_proof", "isar_proof")]
     3.5  
     3.6  val params_for_minimize =
     3.7 -  ["debug", "verbose", "overlord", "full_types", "type_sys", "isar_proof",
     3.8 +  ["debug", "verbose", "overlord", "type_sys", "full_types", "isar_proof",
     3.9     "isar_shrink_factor", "timeout"]
    3.10  
    3.11  val property_dependent_params = ["provers", "full_types", "timeout"]
    3.12 @@ -221,8 +221,8 @@
    3.13      val overlord = lookup_bool "overlord"
    3.14      val provers = lookup_string "provers" |> space_explode " "
    3.15                    |> auto ? single o hd
    3.16 +    val type_sys = lookup_string "type_sys"
    3.17      val full_types = lookup_bool "full_types"
    3.18 -    val type_sys = lookup_string "type_sys"
    3.19      val explicit_apply = lookup_bool "explicit_apply"
    3.20      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    3.21      val max_relevant = lookup_int_option "max_relevant"
    3.22 @@ -232,7 +232,7 @@
    3.23      val expect = lookup_string "expect"
    3.24    in
    3.25      {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
    3.26 -     provers = provers, full_types = full_types, type_sys = type_sys,
    3.27 +     provers = provers, type_sys = type_sys, full_types = full_types,
    3.28       explicit_apply = explicit_apply,
    3.29       relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    3.30       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
     4.3 @@ -20,8 +20,8 @@
     4.4       verbose: bool,
     4.5       overlord: bool,
     4.6       provers: string list,
     4.7 +     type_sys: string,
     4.8       full_types: bool,
     4.9 -     type_sys: string,
    4.10       explicit_apply: bool,
    4.11       relevance_thresholds: real * real,
    4.12       max_relevant: int option,
    4.13 @@ -204,8 +204,8 @@
    4.14     verbose: bool,
    4.15     overlord: bool,
    4.16     provers: string list,
    4.17 +   type_sys: string,
    4.18     full_types: bool,
    4.19 -   type_sys: string,
    4.20     explicit_apply: bool,
    4.21     relevance_thresholds: real * real,
    4.22     max_relevant: int option,
    4.23 @@ -271,7 +271,7 @@
    4.24  fun run_atp auto atp_name
    4.25          ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
    4.26           known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
    4.27 -        ({debug, verbose, overlord, full_types, type_sys, explicit_apply,
    4.28 +        ({debug, verbose, overlord, type_sys, full_types, explicit_apply,
    4.29            isar_proof, isar_shrink_factor, timeout, ...} : params)
    4.30          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
    4.31    let
    4.32 @@ -398,7 +398,7 @@
    4.33          NONE =>
    4.34          proof_text isar_proof
    4.35              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    4.36 -            (proof_banner auto, full_types, minimize_command, tstplike_proof,
    4.37 +            (proof_banner auto, type_sys, minimize_command, tstplike_proof,
    4.38               fact_names, goal, subgoal)
    4.39          |>> (fn message =>
    4.40                  message ^