Metis code cleanup
authorblanchet
Mon Jun 06 20:56:06 2011 +0200 (2011-06-06)
changeset 43212050a03afe024
parent 43211 77c432fe28ff
child 43213 e1fdd27e0c98
Metis code cleanup
src/HOL/Metis_Examples/Proxies.thy
src/HOL/Metis_Examples/Type_Encodings.thy
src/HOL/Mirabelle/Tools/mirabelle_metis.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP/atp_reconstruct.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactics.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/ex/CASC_Setup.thy
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:36:36 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:56:06 2011 +0200
     1.3 @@ -24,24 +24,24 @@
     1.4  
     1.5  lemma "inc \<noteq> (\<lambda>y. 0)"
     1.6  sledgehammer [expect = some] (inc_def plus_1_not_0)
     1.7 -by (new_metis_exhaust inc_def plus_1_not_0)
     1.8 +by (metis_exhaust inc_def plus_1_not_0)
     1.9  
    1.10  lemma "inc = (\<lambda>y. y + 1)"
    1.11  sledgehammer [expect = some] (inc_def)
    1.12 -by (new_metis_exhaust inc_def)
    1.13 +by (metis_exhaust inc_def)
    1.14  
    1.15  definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    1.16  "add_swap = (\<lambda>x y. y + x)"
    1.17  
    1.18  lemma "add_swap m n = n + m"
    1.19  sledgehammer [expect = some] (add_swap_def)
    1.20 -by (new_metis_exhaust add_swap_def)
    1.21 +by (metis_exhaust add_swap_def)
    1.22  
    1.23  definition "A = {xs\<Colon>'a list. True}"
    1.24  
    1.25  lemma "xs \<in> A"
    1.26  sledgehammer [expect = some]
    1.27 -by (new_metis_exhaust A_def Collect_def mem_def)
    1.28 +by (metis_exhaust A_def Collect_def mem_def)
    1.29  
    1.30  definition "B (y::int) \<equiv> y \<le> 0"
    1.31  definition "C (y::int) \<equiv> y \<le> 1"
    1.32 @@ -51,7 +51,7 @@
    1.33  
    1.34  lemma "B \<subseteq> C"
    1.35  sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some]
    1.36 -by (new_metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
    1.37 +by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
    1.38  
    1.39  
    1.40  text {* Proxies for logical constants *}
    1.41 @@ -78,7 +78,7 @@
    1.42  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.43  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.44  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.45 -by (new_metis_exhaust id_apply)
    1.46 +by (metis_exhaust id_apply)
    1.47  
    1.48  lemma "\<not> id False"
    1.49  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.50 @@ -90,7 +90,7 @@
    1.51  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.52  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.53  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.54 -by (new_metis_exhaust id_apply)
    1.55 +by (metis_exhaust id_apply)
    1.56  
    1.57  lemma "x = id True \<or> x = id False"
    1.58  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.59 @@ -102,7 +102,7 @@
    1.60  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.61  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.62  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.63 -by (new_metis_exhaust id_apply)
    1.64 +by (metis_exhaust id_apply)
    1.65  
    1.66  lemma "id x = id True \<or> id x = id False"
    1.67  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.68 @@ -114,7 +114,7 @@
    1.69  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.70  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.71  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.72 -by (new_metis_exhaust id_apply)
    1.73 +by (metis_exhaust id_apply)
    1.74  
    1.75  lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
    1.76  sledgehammer [type_sys = erased, expect = none] ()
    1.77 @@ -139,7 +139,7 @@
    1.78  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.79  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.80  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.81 -by (new_metis_exhaust id_apply)
    1.82 +by (metis_exhaust id_apply)
    1.83  
    1.84  lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
    1.85  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.86 @@ -151,7 +151,7 @@
    1.87  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.88  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.89  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.90 -by (new_metis_exhaust id_apply)
    1.91 +by (metis_exhaust id_apply)
    1.92  
    1.93  lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
    1.94  sledgehammer [type_sys = erased, expect = some] (id_apply)
    1.95 @@ -163,7 +163,7 @@
    1.96  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
    1.97  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
    1.98  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
    1.99 -by (new_metis_exhaust id_apply)
   1.100 +by (metis_exhaust id_apply)
   1.101  
   1.102  lemma "id (a \<and> b) \<Longrightarrow> id a"
   1.103  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.104 @@ -175,7 +175,7 @@
   1.105  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.106  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.107  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.108 -by (new_metis_exhaust id_apply)
   1.109 +by (metis_exhaust id_apply)
   1.110  
   1.111  lemma "id (a \<and> b) \<Longrightarrow> id b"
   1.112  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.113 @@ -187,7 +187,7 @@
   1.114  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.115  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.116  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.117 -by (new_metis_exhaust id_apply)
   1.118 +by (metis_exhaust id_apply)
   1.119  
   1.120  lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
   1.121  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.122 @@ -199,7 +199,7 @@
   1.123  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.124  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.125  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.126 -by (new_metis_exhaust id_apply)
   1.127 +by (metis_exhaust id_apply)
   1.128  
   1.129  lemma "id a \<Longrightarrow> id (a \<or> b)"
   1.130  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.131 @@ -211,7 +211,7 @@
   1.132  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.133  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.134  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.135 -by (new_metis_exhaust id_apply)
   1.136 +by (metis_exhaust id_apply)
   1.137  
   1.138  lemma "id b \<Longrightarrow> id (a \<or> b)"
   1.139  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.140 @@ -223,7 +223,7 @@
   1.141  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.142  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.143  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.144 -by (new_metis_exhaust id_apply)
   1.145 +by (metis_exhaust id_apply)
   1.146  
   1.147  lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
   1.148  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.149 @@ -235,7 +235,7 @@
   1.150  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.151  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.152  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.153 -by (new_metis_exhaust id_apply)
   1.154 +by (metis_exhaust id_apply)
   1.155  
   1.156  lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
   1.157  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.158 @@ -247,7 +247,7 @@
   1.159  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.160  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.161  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.162 -by (new_metis_exhaust id_apply)
   1.163 +by (metis_exhaust id_apply)
   1.164  
   1.165  lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
   1.166  sledgehammer [type_sys = erased, expect = some] (id_apply)
   1.167 @@ -259,6 +259,6 @@
   1.168  sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
   1.169  sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
   1.170  sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
   1.171 -by (new_metis_exhaust id_apply)
   1.172 +by (metis_exhaust id_apply)
   1.173  
   1.174  end
     2.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jun 06 20:36:36 2011 +0200
     2.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Jun 06 20:56:06 2011 +0200
     2.3 @@ -69,47 +69,47 @@
     2.4     "mangled_tags_heavy!",
     2.5     "simple!"]
     2.6  
     2.7 -fun new_metis_exhaust_tac ctxt ths =
     2.8 +fun metis_exhaust_tac ctxt ths =
     2.9    let
    2.10      fun tac [] st = all_tac st
    2.11        | tac (type_sys :: type_syss) st =
    2.12          st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
    2.13             |> ((if null type_syss then all_tac else rtac @{thm fork} 1)
    2.14 -               THEN Metis_Tactics.new_metis_tac [type_sys] ctxt ths 1
    2.15 +               THEN Metis_Tactics.metis_tac [type_sys] ctxt ths 1
    2.16                 THEN COND (has_fewer_prems 2) all_tac no_tac
    2.17                 THEN tac type_syss)
    2.18    in tac end
    2.19  *}
    2.20  
    2.21 -method_setup new_metis_exhaust = {*
    2.22 +method_setup metis_exhaust = {*
    2.23    Attrib.thms >>
    2.24 -    (fn ths => fn ctxt => SIMPLE_METHOD (new_metis_exhaust_tac ctxt ths type_syss))
    2.25 +    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss))
    2.26  *} "exhaustively run the new Metis with all type encodings"
    2.27  
    2.28  
    2.29  text {* Miscellaneous tests *}
    2.30  
    2.31  lemma "x = y \<Longrightarrow> y = x"
    2.32 -by new_metis_exhaust
    2.33 +by metis_exhaust
    2.34  
    2.35  lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
    2.36 -by (new_metis_exhaust last.simps)
    2.37 +by (metis_exhaust last.simps)
    2.38  
    2.39  lemma "map Suc [0] = [Suc 0]"
    2.40 -by (new_metis_exhaust map.simps)
    2.41 +by (metis_exhaust map.simps)
    2.42  
    2.43  lemma "map Suc [1 + 1] = [Suc 2]"
    2.44 -by (new_metis_exhaust map.simps nat_1_add_1)
    2.45 +by (metis_exhaust map.simps nat_1_add_1)
    2.46  
    2.47  lemma "map Suc [2] = [Suc (1 + 1)]"
    2.48 -by (new_metis_exhaust map.simps nat_1_add_1)
    2.49 +by (metis_exhaust map.simps nat_1_add_1)
    2.50  
    2.51  definition "null xs = (xs = [])"
    2.52  
    2.53  lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
    2.54 -by (new_metis_exhaust null_def)
    2.55 +by (metis_exhaust null_def)
    2.56  
    2.57  lemma "(0::nat) + 0 = 0"
    2.58 -by (new_metis_exhaust arithmetic_simps(38))
    2.59 +by (metis_exhaust arithmetic_simps(38))
    2.60  
    2.61  end
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Jun 06 20:36:36 2011 +0200
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Jun 06 20:56:06 2011 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4  
     3.5      val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
     3.6  
     3.7 -    fun metis ctxt = Metis_Tactics.new_metis_tac [] ctxt (thms @ facts)
     3.8 +    fun metis ctxt = Metis_Tactics.metis_tac [] ctxt (thms @ facts)
     3.9    in
    3.10      (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
    3.11      |> prefix (metis_tag id)
     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:36 2011 +0200
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:56:06 2011 +0200
     4.3 @@ -542,9 +542,9 @@
     4.4         else if !reconstructor = "smt" then
     4.5           SMT_Solver.smt_tac
     4.6         else if full orelse !reconstructor = "metisFT" then
     4.7 -         Metis_Tactics.new_metisFT_tac
     4.8 +         Metis_Tactics.metisFT_tac
     4.9         else
    4.10 -         Metis_Tactics.new_metis_tac []) ctxt thms
    4.11 +         Metis_Tactics.metis_tac []) ctxt thms
    4.12      fun apply_reconstructor thms =
    4.13        Mirabelle.can_apply timeout (do_reconstructor thms) st
    4.14  
     5.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:36 2011 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:56:06 2011 +0200
     5.3 @@ -427,7 +427,10 @@
     5.4  fun term_from_atp ctxt textual sym_tab =
     5.5    let
     5.6      val thy = Proof_Context.theory_of ctxt
     5.7 -    (* see also "mk_var" in "Metis_Reconstruct" *)
     5.8 +    (* For Metis, we use 1 rather than 0 because variable references in clauses
     5.9 +       may otherwise conflict with variable constraints in the goal. At least,
    5.10 +       type inference often fails otherwise. See also "axiom_inference" in
    5.11 +       "Metis_Reconstruct". *)
    5.12      val var_index = if textual then 0 else 1
    5.13      fun do_term extra_ts opt_T u =
    5.14        case u of
     6.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:36 2011 +0200
     6.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:56:06 2011 +0200
     6.3 @@ -9,8 +9,6 @@
     6.4  
     6.5  signature METIS_RECONSTRUCT =
     6.6  sig
     6.7 -  type mode = Metis_Translate.mode
     6.8 -
     6.9    exception METIS of string * string
    6.10  
    6.11    val trace : bool Config.T
    6.12 @@ -23,7 +21,7 @@
    6.13    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    6.14    val untyped_aconv : term * term -> bool
    6.15    val replay_one_inference :
    6.16 -    Proof.context -> mode -> (string * term) list -> int Symtab.table
    6.17 +    Proof.context -> (string * term) list -> int Symtab.table
    6.18      -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    6.19      -> (Metis_Thm.thm * thm) list
    6.20    val discharge_skolem_premises :
    6.21 @@ -65,154 +63,6 @@
    6.22    | types_of (SomeTerm _ :: tts) = types_of tts
    6.23    | types_of (SomeType T :: tts) = T :: types_of tts
    6.24  
    6.25 -fun apply_list rator nargs rands =
    6.26 -  let val trands = terms_of rands
    6.27 -  in  if length trands = nargs then SomeTerm (list_comb(rator, trands))
    6.28 -      else raise Fail
    6.29 -        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
    6.30 -          " expected " ^ string_of_int nargs ^
    6.31 -          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
    6.32 -  end;
    6.33 -
    6.34 -fun infer_types ctxt =
    6.35 -  Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    6.36 -
    6.37 -(* We use 1 rather than 0 because variable references in clauses may otherwise
    6.38 -   conflict with variable constraints in the goal...at least, type inference
    6.39 -   often fails otherwise. See also "axiom_inference" below. *)
    6.40 -fun make_var (w, T) = Var ((w, 1), T)
    6.41 -
    6.42 -(*Remove the "apply" operator from an HO term*)
    6.43 -fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t
    6.44 -  | strip_happ args x = (x, args)
    6.45 -
    6.46 -fun hol_type_from_metis_term _ (Metis_Term.Var v) =
    6.47 -     (case strip_prefix_and_unascii tvar_prefix v of
    6.48 -          SOME w => make_tvar w
    6.49 -        | NONE   => make_tvar v)
    6.50 -  | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
    6.51 -     (case strip_prefix_and_unascii type_const_prefix x of
    6.52 -          SOME tc => Type (invert_const tc,
    6.53 -                           map (hol_type_from_metis_term ctxt) tys)
    6.54 -        | NONE    =>
    6.55 -      case strip_prefix_and_unascii tfree_prefix x of
    6.56 -          SOME tf => make_tfree ctxt tf
    6.57 -        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
    6.58 -
    6.59 -(*Maps metis terms to isabelle terms*)
    6.60 -fun hol_term_from_metis_PT ctxt fol_tm =
    6.61 -  let val thy = Proof_Context.theory_of ctxt
    6.62 -      val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
    6.63 -                                       Metis_Term.toString fol_tm)
    6.64 -      fun tm_to_tt (Metis_Term.Var v) =
    6.65 -             (case strip_prefix_and_unascii tvar_prefix v of
    6.66 -                  SOME w => SomeType (make_tvar w)
    6.67 -                | NONE =>
    6.68 -              case strip_prefix_and_unascii schematic_var_prefix v of
    6.69 -                  SOME w => SomeTerm (make_var (w, HOLogic.typeT))
    6.70 -                | NONE   => SomeTerm (make_var (v, HOLogic.typeT)))
    6.71 -                    (*Var from Metis with a name like _nnn; possibly a type variable*)
    6.72 -        | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
    6.73 -        | tm_to_tt (t as Metis_Term.Fn (".", _)) =
    6.74 -            let val (rator,rands) = strip_happ [] t in
    6.75 -              case rator of
    6.76 -                Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
    6.77 -              | _ => case tm_to_tt rator of
    6.78 -                         SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
    6.79 -                       | _ => raise Fail "tm_to_tt: HO application"
    6.80 -            end
    6.81 -        | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
    6.82 -      and applic_to_tt ("=",ts) =
    6.83 -            SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
    6.84 -        | applic_to_tt (a,ts) =
    6.85 -            case strip_prefix_and_unascii const_prefix a of
    6.86 -                SOME b =>
    6.87 -                  let
    6.88 -                    val c = b |> invert_const |> unproxify_const
    6.89 -                    val ntypes = num_type_args thy c
    6.90 -                    val nterms = length ts - ntypes
    6.91 -                    val tts = map tm_to_tt ts
    6.92 -                    val tys = types_of (List.take(tts,ntypes))
    6.93 -                    val t =
    6.94 -                      if String.isPrefix new_skolem_const_prefix c then
    6.95 -                        Var ((new_skolem_var_name_from_const c, 1),
    6.96 -                             Type_Infer.paramify_vars (tl tys ---> hd tys))
    6.97 -                      else
    6.98 -                        Const (c, dummyT)
    6.99 -                  in if length tys = ntypes then
   6.100 -                         apply_list t nterms (List.drop(tts,ntypes))
   6.101 -                     else
   6.102 -                       raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^
   6.103 -                                   " but gets " ^ string_of_int (length tys) ^
   6.104 -                                   " type arguments\n" ^
   6.105 -                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   6.106 -                                   " the terms are \n" ^
   6.107 -                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   6.108 -                     end
   6.109 -              | NONE => (*Not a constant. Is it a type constructor?*)
   6.110 -            case strip_prefix_and_unascii type_const_prefix a of
   6.111 -                SOME b =>
   6.112 -                SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
   6.113 -              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   6.114 -            case strip_prefix_and_unascii tfree_prefix a of
   6.115 -                SOME b => SomeType (make_tfree ctxt b)
   6.116 -              | NONE => (*a fixed variable? They are Skolem functions.*)
   6.117 -            case strip_prefix_and_unascii fixed_var_prefix a of
   6.118 -                SOME b =>
   6.119 -                  let val opr = Free (b, HOLogic.typeT)
   6.120 -                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
   6.121 -              | NONE => raise Fail ("unexpected metis function: " ^ a)
   6.122 -  in
   6.123 -    case tm_to_tt fol_tm of
   6.124 -      SomeTerm t => t
   6.125 -    | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
   6.126 -  end
   6.127 -
   6.128 -(*Maps fully-typed metis terms to isabelle terms*)
   6.129 -fun hol_term_from_metis_FT ctxt fol_tm =
   6.130 -  let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
   6.131 -                                       Metis_Term.toString fol_tm)
   6.132 -      fun do_const c =
   6.133 -        let val c = c |> invert_const |> unproxify_const in
   6.134 -          if String.isPrefix new_skolem_const_prefix c then
   6.135 -            Var ((new_skolem_var_name_from_const c, 1), dummyT)
   6.136 -          else
   6.137 -            Const (c, dummyT)
   6.138 -        end
   6.139 -      fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =
   6.140 -             (case strip_prefix_and_unascii schematic_var_prefix v of
   6.141 -                  SOME w =>  make_var (w, dummyT)
   6.142 -                | NONE   => make_var (v, dummyT))
   6.143 -        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =
   6.144 -            Const (@{const_name HOL.eq}, HOLogic.typeT)
   6.145 -        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =
   6.146 -           (case strip_prefix_and_unascii const_prefix x of
   6.147 -                SOME c => do_const c
   6.148 -              | NONE => (*Not a constant. Is it a fixed variable??*)
   6.149 -            case strip_prefix_and_unascii fixed_var_prefix x of
   6.150 -                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
   6.151 -              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
   6.152 -        | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (".", [tm1,tm2]), _])) =
   6.153 -            cvt tm1 $ cvt tm2
   6.154 -        | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   6.155 -            cvt tm1 $ cvt tm2
   6.156 -        | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   6.157 -        | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
   6.158 -            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
   6.159 -        | cvt (t as Metis_Term.Fn (x, [])) =
   6.160 -           (case strip_prefix_and_unascii const_prefix x of
   6.161 -                SOME c => do_const c
   6.162 -              | NONE => (*Not a constant. Is it a fixed variable??*)
   6.163 -            case strip_prefix_and_unascii fixed_var_prefix x of
   6.164 -                SOME v => Free (v, dummyT)
   6.165 -              | NONE => (trace_msg ctxt (fn () =>
   6.166 -                                      "hol_term_from_metis_FT bad const: " ^ x);
   6.167 -                         hol_term_from_metis_PT ctxt t))
   6.168 -        | cvt t = (trace_msg ctxt (fn () =>
   6.169 -                   "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
   6.170 -                   hol_term_from_metis_PT ctxt t)
   6.171 -  in fol_tm |> cvt end
   6.172 -
   6.173  fun atp_name_from_metis s =
   6.174    case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
   6.175      SOME ((s, _), (_, swap)) => (s, swap)
   6.176 @@ -223,15 +73,8 @@
   6.177      end
   6.178    | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
   6.179  
   6.180 -fun hol_term_from_metis_MX ctxt sym_tab =
   6.181 -  atp_term_from_metis
   6.182 -  #> term_from_atp ctxt false sym_tab NONE
   6.183 -
   6.184 -fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt
   6.185 -  | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt
   6.186 -  | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
   6.187 -  | hol_term_from_metis ctxt (Type_Sys _) sym_tab =
   6.188 -    hol_term_from_metis_MX ctxt sym_tab
   6.189 +fun hol_term_from_metis ctxt sym_tab =
   6.190 +  atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
   6.191  
   6.192  fun atp_literal_from_metis (pos, atom) =
   6.193    atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
   6.194 @@ -241,7 +84,7 @@
   6.195  
   6.196  fun reveal_old_skolems_and_infer_types ctxt old_skolems =
   6.197    map (reveal_old_skolem_terms old_skolems)
   6.198 -  #> infer_types ctxt
   6.199 +  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
   6.200  
   6.201  fun hol_clause_from_metis ctxt sym_tab old_skolems =
   6.202    Metis_Thm.clause
   6.203 @@ -250,8 +93,8 @@
   6.204    #> prop_from_atp ctxt false sym_tab
   6.205    #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
   6.206  
   6.207 -fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
   6.208 -  let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
   6.209 +fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
   6.210 +  let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
   6.211        val _ = trace_msg ctxt (fn () => "  calling type inference:")
   6.212        val _ = app (fn t => trace_msg ctxt
   6.213                                       (fn () => Syntax.string_of_term ctxt t)) ts
   6.214 @@ -284,9 +127,9 @@
   6.215  
   6.216  (* INFERENCE RULE: AXIOM *)
   6.217  
   6.218 -(* This causes variables to have an index of 1 by default. See also "make_var"
   6.219 -   above. *)
   6.220 -fun axiom_inference th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)
   6.221 +(* This causes variables to have an index of 1 by default. See also
   6.222 +   "term_from_atp" in "ATP_Reconstruct". *)
   6.223 +val axiom_inference = Thm.incr_indexes 1 oo lookth
   6.224  
   6.225  (* INFERENCE RULE: ASSUME *)
   6.226  
   6.227 @@ -298,10 +141,10 @@
   6.228        val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
   6.229    in  cterm_instantiate substs th  end;
   6.230  
   6.231 -fun assume_inference ctxt mode old_skolems sym_tab atom =
   6.232 +fun assume_inference ctxt old_skolems sym_tab atom =
   6.233    inst_excluded_middle
   6.234        (Proof_Context.theory_of ctxt)
   6.235 -      (singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
   6.236 +      (singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
   6.237                   (Metis_Term.Fn atom))
   6.238  
   6.239  (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
   6.240 @@ -309,7 +152,7 @@
   6.241     sorts. Instead we try to arrange that new TVars are distinct and that types
   6.242     can be inferred from terms. *)
   6.243  
   6.244 -fun inst_inference ctxt mode old_skolems sym_tab th_pairs fsubst th =
   6.245 +fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
   6.246    let val thy = Proof_Context.theory_of ctxt
   6.247        val i_th = lookth th_pairs th
   6.248        val i_th_vars = Term.add_vars (prop_of i_th) []
   6.249 @@ -317,7 +160,7 @@
   6.250        fun subst_translation (x,y) =
   6.251          let val v = find_var x
   6.252              (* We call "reveal_old_skolems_and_infer_types" below. *)
   6.253 -            val t = hol_term_from_metis ctxt mode sym_tab y
   6.254 +            val t = hol_term_from_metis ctxt sym_tab y
   6.255          in  SOME (cterm_of thy (Var v), t)  end
   6.256          handle Option.Option =>
   6.257                 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
   6.258 @@ -441,7 +284,7 @@
   6.259  (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
   6.260  val select_literal = negate_head oo make_last
   6.261  
   6.262 -fun resolve_inference ctxt mode old_skolems sym_tab th_pairs atom th1 th2 =
   6.263 +fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
   6.264    let
   6.265      val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
   6.266      val _ = trace_msg ctxt (fn () =>
   6.267 @@ -457,7 +300,7 @@
   6.268        let
   6.269          val thy = Proof_Context.theory_of ctxt
   6.270          val i_atom =
   6.271 -          singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
   6.272 +          singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
   6.273                      (Metis_Term.Fn atom)
   6.274          val _ = trace_msg ctxt (fn () =>
   6.275                      "  atom: " ^ Syntax.string_of_term ctxt i_atom)
   6.276 @@ -486,10 +329,10 @@
   6.277  val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   6.278  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   6.279  
   6.280 -fun refl_inference ctxt mode old_skolems sym_tab t =
   6.281 +fun refl_inference ctxt old_skolems sym_tab t =
   6.282    let
   6.283      val thy = Proof_Context.theory_of ctxt
   6.284 -    val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t
   6.285 +    val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
   6.286      val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   6.287      val c_t = cterm_incr_types thy refl_idx i_t
   6.288    in cterm_instantiate [(refl_x, c_t)] REFL_THM end
   6.289 @@ -499,19 +342,11 @@
   6.290  val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
   6.291  val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
   6.292  
   6.293 -val metis_eq = Metis_Term.Fn ("=", []);
   6.294 -
   6.295 -(* Equality has no type arguments *)
   6.296 -fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0
   6.297 -  | get_ty_arg_size thy (Const (s, _)) =
   6.298 -    (num_type_args thy s handle TYPE _ => 0)
   6.299 -  | get_ty_arg_size _ _ = 0
   6.300 -
   6.301 -fun equality_inference ctxt mode old_skolems sym_tab (pos, atom) fp fr =
   6.302 +fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
   6.303    let val thy = Proof_Context.theory_of ctxt
   6.304        val m_tm = Metis_Term.Fn atom
   6.305        val [i_atom, i_tm] =
   6.306 -        hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr]
   6.307 +        hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
   6.308        val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   6.309        fun replace_item_list lx 0 (_::ls) = lx::ls
   6.310          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   6.311 @@ -522,53 +357,24 @@
   6.312                       (case t of
   6.313                          SOME t => " fol-term: " ^ Metis_Term.toString t
   6.314                        | NONE => ""))
   6.315 -      fun path_finder_FO tm [] = (tm, Bound 0)
   6.316 -        | path_finder_FO tm (p::ps) =
   6.317 -            let val (tm1,args) = strip_comb tm
   6.318 -                val adjustment = get_ty_arg_size thy tm1
   6.319 -                val p' = if adjustment > p then p else p - adjustment
   6.320 -                val tm_p = nth args p'
   6.321 -                  handle Subscript =>
   6.322 -                         raise METIS ("equality_inference",
   6.323 -                                      string_of_int p ^ " adj " ^
   6.324 -                                      string_of_int adjustment ^ " term " ^
   6.325 -                                      Syntax.string_of_term ctxt tm)
   6.326 -                val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
   6.327 -                                      "  " ^ Syntax.string_of_term ctxt tm_p)
   6.328 -                val (r,t) = path_finder_FO tm_p ps
   6.329 -            in
   6.330 -                (r, list_comb (tm1, replace_item_list t p' args))
   6.331 -            end
   6.332 -      fun path_finder_HO tm [] = (tm, Bound 0)
   6.333 -        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   6.334 -        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   6.335 -        | path_finder_HO tm ps = path_finder_fail tm ps NONE
   6.336 -      fun path_finder_FT tm [] _ = (tm, Bound 0)
   6.337 -        | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) =
   6.338 -            path_finder_FT tm ps t1
   6.339 -        | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
   6.340 -            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   6.341 -        | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
   6.342 -            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   6.343 -        | path_finder_FT tm ps t = path_finder_fail tm ps (SOME t)
   6.344 -      fun path_finder_MX tm [] _ = (tm, Bound 0)
   6.345 -        | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
   6.346 +      fun path_finder tm [] _ = (tm, Bound 0)
   6.347 +        | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
   6.348            let
   6.349              val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix
   6.350                                         #> the #> unmangled_const_name))
   6.351            in
   6.352              if s = metis_predicator orelse s = predicator_name orelse
   6.353                 s = metis_type_tag orelse s = type_tag_name then
   6.354 -              path_finder_MX tm ps (nth ts p)
   6.355 +              path_finder tm ps (nth ts p)
   6.356              else if s = metis_app_op orelse s = app_op_name then
   6.357                let
   6.358                  val (tm1, tm2) = dest_comb tm
   6.359                  val p' = p - (length ts - 2)
   6.360                in
   6.361                  if p' = 0 then
   6.362 -                  path_finder_MX tm1 ps (nth ts p) ||> (fn y => y $ tm2)
   6.363 +                  path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
   6.364                  else
   6.365 -                  path_finder_MX tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
   6.366 +                  path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
   6.367                end
   6.368              else
   6.369                let
   6.370 @@ -581,31 +387,11 @@
   6.371                  val _ = trace_msg ctxt (fn () =>
   6.372                      "path_finder: " ^ string_of_int p ^ "  " ^
   6.373                      Syntax.string_of_term ctxt tm_p)
   6.374 -                val (r, t) = path_finder_MX tm_p ps (nth ts p)
   6.375 +                val (r, t) = path_finder tm_p ps (nth ts p)
   6.376                in (r, list_comb (tm1, replace_item_list t p' args)) end
   6.377            end
   6.378 -        | path_finder_MX tm ps t = path_finder_fail tm ps (SOME t)
   6.379 -      fun path_finder FO tm ps _ = path_finder_FO tm ps
   6.380 -        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
   6.381 -             (*equality: not curried, as other predicates are*)
   6.382 -             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   6.383 -             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   6.384 -        | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
   6.385 -             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   6.386 -        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
   6.387 -                            (Metis_Term.Fn ("=", [t1,t2])) =
   6.388 -             (*equality: not curried, as other predicates are*)
   6.389 -             if p=0 then path_finder_FT tm (0::1::ps)
   6.390 -                          (Metis_Term.Fn (metis_app_op, [Metis_Term.Fn (metis_app_op, [metis_eq,t1]), t2]))
   6.391 -                          (*select first operand*)
   6.392 -             else path_finder_FT tm (p::ps)
   6.393 -                   (Metis_Term.Fn (metis_app_op, [metis_eq, t2]))
   6.394 -                   (*1 selects second operand*)
   6.395 -        | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   6.396 -             (*if not equality, ignore head to skip the hBOOL predicate*)
   6.397 -        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   6.398 -        | path_finder (Type_Sys _) tm ps t = path_finder_MX tm ps t
   6.399 -      val (tm_subst, body) = path_finder mode i_atom fp m_tm
   6.400 +        | path_finder tm ps t = path_finder_fail tm ps (SOME t)
   6.401 +      val (tm_subst, body) = path_finder i_atom fp m_tm
   6.402        val tm_abs = Abs ("x", type_of tm_subst, body)
   6.403        val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   6.404        val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   6.405 @@ -619,21 +405,21 @@
   6.406  
   6.407  val factor = Seq.hd o distinct_subgoals_tac
   6.408  
   6.409 -fun one_step ctxt mode old_skolems sym_tab th_pairs p =
   6.410 +fun one_step ctxt old_skolems sym_tab th_pairs p =
   6.411    case p of
   6.412      (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
   6.413    | (_, Metis_Proof.Assume f_atom) =>
   6.414 -    assume_inference ctxt mode old_skolems sym_tab f_atom
   6.415 +    assume_inference ctxt old_skolems sym_tab f_atom
   6.416    | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
   6.417 -    inst_inference ctxt mode old_skolems sym_tab th_pairs f_subst f_th1
   6.418 +    inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
   6.419      |> factor
   6.420    | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
   6.421 -    resolve_inference ctxt mode old_skolems sym_tab th_pairs f_atom f_th1 f_th2
   6.422 +    resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
   6.423      |> factor
   6.424    | (_, Metis_Proof.Refl f_tm) =>
   6.425 -    refl_inference ctxt mode old_skolems sym_tab f_tm
   6.426 +    refl_inference ctxt old_skolems sym_tab f_tm
   6.427    | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
   6.428 -    equality_inference ctxt mode old_skolems sym_tab f_lit f_p f_r
   6.429 +    equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
   6.430  
   6.431  fun flexflex_first_order th =
   6.432    case Thm.tpairs_of th of
   6.433 @@ -684,7 +470,7 @@
   6.434        end
   6.435    end
   6.436  
   6.437 -fun replay_one_inference ctxt mode old_skolems sym_tab (fol_th, inf) th_pairs =
   6.438 +fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
   6.439    if not (null th_pairs) andalso
   6.440       prop_of (snd (hd th_pairs)) aconv @{prop False} then
   6.441      (* Isabelle sometimes identifies literals (premises) that are distinct in
   6.442 @@ -699,7 +485,7 @@
   6.443                    (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   6.444        val _ = trace_msg ctxt
   6.445                    (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   6.446 -      val th = one_step ctxt mode old_skolems sym_tab th_pairs (fol_th, inf)
   6.447 +      val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
   6.448                 |> flexflex_first_order
   6.449                 |> resynchronize ctxt fol_th
   6.450        val _ = trace_msg ctxt
     7.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:36 2011 +0200
     7.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:56:06 2011 +0200
     7.3 @@ -16,11 +16,8 @@
     7.4    val trace : bool Config.T
     7.5    val verbose : bool Config.T
     7.6    val new_skolemizer : bool Config.T
     7.7 -  val old_metis_tac : Proof.context -> thm list -> int -> tactic
     7.8 -  val old_metisF_tac : Proof.context -> thm list -> int -> tactic
     7.9 -  val old_metisFT_tac : Proof.context -> thm list -> int -> tactic
    7.10 -  val new_metis_tac : string list -> Proof.context -> thm list -> int -> tactic
    7.11 -  val new_metisFT_tac : Proof.context -> thm list -> int -> tactic
    7.12 +  val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
    7.13 +  val metisFT_tac : Proof.context -> thm list -> int -> tactic
    7.14    val setup : theory -> theory
    7.15  end
    7.16  
    7.17 @@ -38,15 +35,12 @@
    7.18  val default_unsound_type_sys = "poly_args"
    7.19  val default_sound_type_sys = "poly_preds_heavy_query"
    7.20  
    7.21 -fun method_call_for_mode HO = (@{binding old_metis}, "")
    7.22 -  | method_call_for_mode FO = (@{binding metisF}, "")
    7.23 -  | method_call_for_mode FT = (@{binding old_metisFT}, "")
    7.24 -  | method_call_for_mode (Type_Sys type_sys) =
    7.25 -    if type_sys = default_sound_type_sys then
    7.26 -      (@{binding metisFT}, "")
    7.27 -    else
    7.28 -      (@{binding metis},
    7.29 -       if type_sys = default_unsound_type_sys then "" else type_sys)
    7.30 +fun method_call_for_type_sys type_sys =
    7.31 +  if type_sys = default_sound_type_sys then
    7.32 +    (@{binding metisFT}, "")
    7.33 +  else
    7.34 +    (@{binding metis},
    7.35 +     if type_sys = default_unsound_type_sys then "" else type_sys)
    7.36  
    7.37  val new_skolemizer =
    7.38    Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    7.39 @@ -92,13 +86,8 @@
    7.40  val resolution_params = {active = active_params, waiting = waiting_params}
    7.41  
    7.42  (* Main function to start Metis proof and reconstruction *)
    7.43 -fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
    7.44 +fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 =
    7.45    let val thy = Proof_Context.theory_of ctxt
    7.46 -      val _ =
    7.47 -        if mode = FO then
    7.48 -          legacy_feature "Old 'metisF' command -- use 'metis' instead"
    7.49 -        else
    7.50 -          ()
    7.51        val new_skolemizer =
    7.52          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    7.53        val th_cls_pairs =
    7.54 @@ -112,8 +101,8 @@
    7.55        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    7.56        val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    7.57        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
    7.58 -      val (mode, sym_tab, {axioms, old_skolems, ...}) =
    7.59 -        prepare_metis_problem ctxt mode cls ths
    7.60 +      val (sym_tab, axioms, old_skolems) =
    7.61 +        prepare_metis_problem ctxt type_sys cls ths
    7.62        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    7.63            reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
    7.64          | get_isa_thm _ (Isa_Raw ith) = ith
    7.65 @@ -121,7 +110,7 @@
    7.66        val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    7.67        val thms = axioms |> map fst
    7.68        val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
    7.69 -      val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
    7.70 +      val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys)
    7.71        val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
    7.72    in
    7.73        case filter (fn t => prop_of t aconv @{prop False}) cls of
    7.74 @@ -136,8 +125,8 @@
    7.75                               (*add constraints arising from converting goal to clause form*)
    7.76                  val proof = Metis_Proof.proof mth
    7.77                  val result =
    7.78 -                  fold (replay_one_inference ctxt' mode old_skolems sym_tab)
    7.79 -                       proof axioms
    7.80 +                  axioms
    7.81 +                  |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof
    7.82                  val used = map_filter (used_axioms axioms) proof
    7.83                  val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    7.84                  val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
    7.85 @@ -166,7 +155,7 @@
    7.86              end
    7.87          | Metis_Resolution.Satisfiable _ =>
    7.88              (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
    7.89 -             if null fallback_modes then
    7.90 +             if null fallback_type_syss then
    7.91                 ()
    7.92               else
    7.93                 raise METIS ("FOL_SOLVE",
    7.94 @@ -174,17 +163,17 @@
    7.95               [])
    7.96    end
    7.97    handle METIS (loc, msg) =>
    7.98 -         case fallback_modes of
    7.99 +         case fallback_type_syss of
   7.100             [] => error ("Failed to replay Metis proof in Isabelle." ^
   7.101                          (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
   7.102                           else ""))
   7.103 -         | mode :: _ =>
   7.104 -           let val (binding, arg) = method_call_for_mode mode in
   7.105 +         | type_sys :: _ =>
   7.106 +           let val (binding, arg) = method_call_for_type_sys type_sys in
   7.107               (verbose_warning ctxt
   7.108                    ("Falling back on " ^
   7.109                     quote (Binding.qualified_name_of binding ^
   7.110                            (arg |> arg <> "" ? enclose " (" ")")) ^ "...");
   7.111 -              FOL_SOLVE fallback_modes ctxt cls ths0)
   7.112 +              FOL_SOLVE fallback_type_syss ctxt cls ths0)
   7.113              end
   7.114  
   7.115  val neg_clausify =
   7.116 @@ -204,12 +193,12 @@
   7.117  val type_has_top_sort =
   7.118    exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   7.119  
   7.120 -fun generic_metis_tac modes ctxt ths i st0 =
   7.121 +fun generic_metis_tac type_syss ctxt ths i st0 =
   7.122    let
   7.123      val _ = trace_msg ctxt (fn () =>
   7.124          "Metis called with theorems\n" ^
   7.125          cat_lines (map (Display.string_of_thm ctxt) ths))
   7.126 -    fun tac clause = resolve_tac (FOL_SOLVE modes ctxt clause ths) 1
   7.127 +    fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
   7.128    in
   7.129      if exists_type type_has_top_sort (prop_of st0) then
   7.130        (verbose_warning ctxt "Proof state contains the universal sort {}";
   7.131 @@ -218,19 +207,12 @@
   7.132        Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
   7.133    end
   7.134  
   7.135 -val old_metis_modes = [HO, FT]
   7.136 -val old_metisF_modes = [FO, FT]
   7.137 -val old_metisFT_modes = [FT]
   7.138 -val new_metis_default_modes =
   7.139 -  map Type_Sys [default_unsound_type_sys, default_sound_type_sys]
   7.140 -val new_metisFT_modes = [Type_Sys default_sound_type_sys]
   7.141 +val metis_default_type_syss = [default_unsound_type_sys, default_sound_type_sys]
   7.142 +val metisFT_type_syss = [default_sound_type_sys]
   7.143  
   7.144 -val old_metis_tac = generic_metis_tac old_metis_modes
   7.145 -val old_metisF_tac = generic_metis_tac old_metisF_modes
   7.146 -val old_metisFT_tac = generic_metis_tac old_metisFT_modes
   7.147 -fun new_metis_tac [] = generic_metis_tac new_metis_default_modes
   7.148 -  | new_metis_tac type_syss = generic_metis_tac (map Type_Sys type_syss)
   7.149 -val new_metisFT_tac = generic_metis_tac new_metisFT_modes
   7.150 +fun metis_tac [] = generic_metis_tac metis_default_type_syss
   7.151 +  | metis_tac type_syss = generic_metis_tac type_syss
   7.152 +val metisFT_tac = generic_metis_tac metisFT_type_syss
   7.153  
   7.154  (* Whenever "X" has schematic type variables, we treat "using X by metis" as
   7.155     "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
   7.156 @@ -240,33 +222,30 @@
   7.157  val has_tvar =
   7.158    exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   7.159  
   7.160 -fun method modes (type_sys, ths) ctxt facts =
   7.161 +fun method type_syss (type_sys, ths) ctxt facts =
   7.162    let
   7.163      val (schem_facts, nonschem_facts) = List.partition has_tvar facts
   7.164 -    val modes = type_sys |> Option.map (single o Type_Sys) |> the_default modes
   7.165 +    val type_syss = type_sys |> Option.map single |> the_default type_syss
   7.166    in
   7.167      HEADGOAL (Method.insert_tac nonschem_facts THEN'
   7.168 -              CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths))
   7.169 +              CHANGED_PROP
   7.170 +              o generic_metis_tac type_syss ctxt (schem_facts @ ths))
   7.171    end
   7.172  
   7.173 -fun setup_method (modes as mode :: _) =
   7.174 -  (if modes = new_metis_default_modes then
   7.175 +fun setup_method (type_syss as type_sys :: _) =
   7.176 +  (if type_syss = metis_default_type_syss then
   7.177       (Args.parens Parse.short_ident
   7.178        >> (fn s => if s = full_typesN then default_sound_type_sys else s))
   7.179       |> Scan.option |> Scan.lift
   7.180     else
   7.181       Scan.succeed NONE)
   7.182 -  -- Attrib.thms >> (METHOD oo method modes)
   7.183 -  |> Method.setup (fst (method_call_for_mode mode))
   7.184 +  -- Attrib.thms >> (METHOD oo method type_syss)
   7.185 +  |> Method.setup (fst (method_call_for_type_sys type_sys))
   7.186  
   7.187  val setup =
   7.188 -  [(old_metis_modes, "Metis for FOL and HOL problems"),
   7.189 -   (old_metisF_modes, "Metis for FOL problems (legacy)"),
   7.190 -   (old_metisFT_modes,
   7.191 -    "Metis for FOL/HOL problems with fully-typed translation"),
   7.192 -   (new_metis_default_modes, "Metis for FOL and HOL problems (experimental)"),
   7.193 -   (new_metisFT_modes,
   7.194 -    "Metis for FOL/HOL problems with fully-typed translation (experimental)")]
   7.195 +  [(metis_default_type_syss, "Metis for FOL and HOL problems"),
   7.196 +   (metisFT_type_syss,
   7.197 +    "Metis for FOL/HOL problems with fully-typed translation")]
   7.198    |> fold (uncurry setup_method)
   7.199  
   7.200  end;
     8.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:36 2011 +0200
     8.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:56:06 2011 +0200
     8.3 @@ -11,17 +11,10 @@
     8.4  sig
     8.5    type type_literal = ATP_Translate.type_literal
     8.6  
     8.7 -  datatype mode = FO | HO | FT | Type_Sys of string
     8.8 -
     8.9    datatype isa_thm =
    8.10      Isa_Reflexive_or_Trivial |
    8.11      Isa_Raw of thm
    8.12  
    8.13 -  type metis_problem =
    8.14 -    {axioms : (Metis_Thm.thm * isa_thm) list,
    8.15 -     tfrees : type_literal list,
    8.16 -     old_skolems : (string * term) list}
    8.17 -
    8.18    val metis_equal : string
    8.19    val metis_predicator : string
    8.20    val metis_app_op : string
    8.21 @@ -29,10 +22,9 @@
    8.22    val metis_generated_var_prefix : string
    8.23    val metis_name_table : ((string * int) * (string * bool)) list
    8.24    val reveal_old_skolem_terms : (string * term) list -> term -> term
    8.25 -  val string_of_mode : mode -> string
    8.26    val prepare_metis_problem :
    8.27 -    Proof.context -> mode -> thm list -> thm list
    8.28 -    -> mode * int Symtab.table * metis_problem
    8.29 +    Proof.context -> string -> thm list -> thm list
    8.30 +    -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
    8.31  end
    8.32  
    8.33  structure Metis_Translate : METIS_TRANSLATE =
    8.34 @@ -54,20 +46,6 @@
    8.35     ((prefixed_app_op_name, 2), (metis_app_op, false)),
    8.36     ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
    8.37  
    8.38 -fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
    8.39 -  | predicate_of thy (t, pos) =
    8.40 -    (combterm_from_term thy [] (Envir.eta_contract t), pos)
    8.41 -
    8.42 -fun literals_of_term1 args thy (@{const Trueprop} $ P) =
    8.43 -    literals_of_term1 args thy P
    8.44 -  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
    8.45 -    literals_of_term1 (literals_of_term1 args thy P) thy Q
    8.46 -  | literals_of_term1 (lits, ts) thy P =
    8.47 -    let val ((pred, ts'), pol) = predicate_of thy (P, true) in
    8.48 -      ((pol, pred) :: lits, union (op =) ts ts')
    8.49 -    end
    8.50 -val literals_of_term = literals_of_term1 ([], [])
    8.51 -
    8.52  fun old_skolem_const_name i j num_T_args =
    8.53    old_skolem_const_prefix ^ Long_Name.separator ^
    8.54    (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
    8.55 @@ -114,127 +92,6 @@
    8.56  
    8.57  
    8.58  (* ------------------------------------------------------------------------- *)
    8.59 -(* HOL to FOL  (Isabelle to Metis)                                           *)
    8.60 -(* ------------------------------------------------------------------------- *)
    8.61 -
    8.62 -(* first-order, higher-order, fully-typed, ATP type system *)
    8.63 -datatype mode = FO | HO | FT | Type_Sys of string
    8.64 -
    8.65 -fun string_of_mode FO = "FO"
    8.66 -  | string_of_mode HO = "HO"
    8.67 -  | string_of_mode FT = "FT"
    8.68 -  | string_of_mode (Type_Sys type_sys) = "Type_Sys " ^ type_sys
    8.69 -
    8.70 -fun fn_isa_to_met_sublevel "equal" = "c_fequal"
    8.71 -  | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
    8.72 -  | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
    8.73 -  | fn_isa_to_met_sublevel "c_Not" = "c_fNot"
    8.74 -  | fn_isa_to_met_sublevel "c_conj" = "c_fconj"
    8.75 -  | fn_isa_to_met_sublevel "c_disj" = "c_fdisj"
    8.76 -  | fn_isa_to_met_sublevel "c_implies" = "c_fimplies"
    8.77 -  | fn_isa_to_met_sublevel x = x
    8.78 -
    8.79 -fun fn_isa_to_met_toplevel "equal" = metis_equal
    8.80 -  | fn_isa_to_met_toplevel x = x
    8.81 -
    8.82 -fun metis_lit b c args = (b, (c, args));
    8.83 -
    8.84 -fun metis_term_from_typ (Type (s, Ts)) =
    8.85 -    Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts)
    8.86 -  | metis_term_from_typ (TFree (s, _)) =
    8.87 -    Metis_Term.Fn (make_fixed_type_var s, [])
    8.88 -  | metis_term_from_typ (TVar (x, _)) =
    8.89 -    Metis_Term.Var (make_schematic_type_var x)
    8.90 -
    8.91 -(*These two functions insert type literals before the real literals. That is the
    8.92 -  opposite order from TPTP linkup, but maybe OK.*)
    8.93 -
    8.94 -fun hol_term_to_fol_FO tm =
    8.95 -  case strip_combterm_comb tm of
    8.96 -      (CombConst ((c, _), _, Ts), tms) =>
    8.97 -        let val tyargs = map metis_term_from_typ Ts
    8.98 -            val args = map hol_term_to_fol_FO tms
    8.99 -        in Metis_Term.Fn (c, tyargs @ args) end
   8.100 -    | (CombVar ((v, _), _), []) => Metis_Term.Var v
   8.101 -    | _ => raise Fail "non-first-order combterm"
   8.102 -
   8.103 -fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) =
   8.104 -    Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts)
   8.105 -  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
   8.106 -  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
   8.107 -    Metis_Term.Fn (metis_app_op, map hol_term_to_fol_HO [tm1, tm2])
   8.108 -
   8.109 -(*The fully-typed translation, to avoid type errors*)
   8.110 -fun tag_with_type tm T =
   8.111 -  Metis_Term.Fn (metis_type_tag, [tm, metis_term_from_typ T])
   8.112 -
   8.113 -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) =
   8.114 -    tag_with_type (Metis_Term.Var s) ty
   8.115 -  | hol_term_to_fol_FT (CombConst ((a, _), ty, _)) =
   8.116 -    tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty
   8.117 -  | hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) =
   8.118 -    tag_with_type
   8.119 -        (Metis_Term.Fn (metis_app_op, map hol_term_to_fol_FT [tm1, tm2]))
   8.120 -        (combtyp_of tm)
   8.121 -
   8.122 -fun hol_literal_to_fol FO (pos, tm) =
   8.123 -      let
   8.124 -        val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm
   8.125 -        val tylits = if p = "equal" then [] else map metis_term_from_typ Ts
   8.126 -        val lits = map hol_term_to_fol_FO tms
   8.127 -      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
   8.128 -  | hol_literal_to_fol HO (pos, tm) =
   8.129 -     (case strip_combterm_comb tm of
   8.130 -          (CombConst(("equal", _), _, _), tms) =>
   8.131 -            metis_lit pos metis_equal (map hol_term_to_fol_HO tms)
   8.132 -        | _ => metis_lit pos metis_predicator [hol_term_to_fol_HO tm])
   8.133 -  | hol_literal_to_fol FT (pos, tm) =
   8.134 -     (case strip_combterm_comb tm of
   8.135 -          (CombConst(("equal", _), _, _), tms) =>
   8.136 -            metis_lit pos metis_equal (map hol_term_to_fol_FT tms)
   8.137 -        | _ => metis_lit pos metis_predicator [hol_term_to_fol_FT tm])
   8.138 -
   8.139 -fun literals_of_hol_term thy mode t =
   8.140 -  let val (lits, types_sorts) = literals_of_term thy t in
   8.141 -    (map (hol_literal_to_fol mode) lits, types_sorts)
   8.142 -  end
   8.143 -
   8.144 -(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   8.145 -fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
   8.146 -    metis_lit pos s [Metis_Term.Var s']
   8.147 -  | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
   8.148 -    metis_lit pos s [Metis_Term.Fn (s',[])]
   8.149 -
   8.150 -fun has_default_sort _ (TVar _) = false
   8.151 -  | has_default_sort ctxt (TFree (x, s)) =
   8.152 -    (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
   8.153 -
   8.154 -fun metis_of_tfree tf =
   8.155 -  Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
   8.156 -
   8.157 -fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th =
   8.158 -  let
   8.159 -    val thy = Proof_Context.theory_of ctxt
   8.160 -    val (old_skolems, (mlits, types_sorts)) =
   8.161 -     th |> prop_of |> Logic.strip_imp_concl
   8.162 -        |> conceal_old_skolem_terms j old_skolems
   8.163 -        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   8.164 -  in
   8.165 -    if is_conjecture then
   8.166 -      (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
   8.167 -       raw_type_literals_for_types types_sorts, old_skolems)
   8.168 -    else
   8.169 -      let
   8.170 -        val tylits = types_sorts |> filter_out (has_default_sort ctxt)
   8.171 -                                 |> raw_type_literals_for_types
   8.172 -        val mtylits = map (metis_of_type_literals false) tylits
   8.173 -      in
   8.174 -        (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
   8.175 -         old_skolems)
   8.176 -      end
   8.177 -  end;
   8.178 -
   8.179 -(* ------------------------------------------------------------------------- *)
   8.180  (* Logic maps manage the interface between HOL and first-order logic.        *)
   8.181  (* ------------------------------------------------------------------------- *)
   8.182  
   8.183 @@ -242,56 +99,6 @@
   8.184    Isa_Reflexive_or_Trivial |
   8.185    Isa_Raw of thm
   8.186  
   8.187 -type metis_problem =
   8.188 -  {axioms : (Metis_Thm.thm * isa_thm) list,
   8.189 -   tfrees : type_literal list,
   8.190 -   old_skolems : (string * term) list}
   8.191 -
   8.192 -fun is_quasi_fol_clause thy =
   8.193 -  Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
   8.194 -
   8.195 -(*Extract TFree constraints from context to include as conjecture clauses*)
   8.196 -fun init_tfrees ctxt =
   8.197 -  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
   8.198 -    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
   8.199 -    |> raw_type_literals_for_types
   8.200 -  end;
   8.201 -
   8.202 -fun const_in_metis c (pred, tm_list) =
   8.203 -  let
   8.204 -    fun in_mterm (Metis_Term.Var _) = false
   8.205 -      | in_mterm (Metis_Term.Fn (nm, tm_list)) =
   8.206 -        c = nm orelse exists in_mterm tm_list
   8.207 -  in c = pred orelse exists in_mterm tm_list end
   8.208 -
   8.209 -(* ARITY CLAUSE *)
   8.210 -fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
   8.211 -    metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
   8.212 -  | m_arity_cls (TVarLit ((c, _), (s, _))) =
   8.213 -    metis_lit false c [Metis_Term.Var s]
   8.214 -(* TrueI is returned as the Isabelle counterpart because there isn't any. *)
   8.215 -fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) =
   8.216 -  (TrueI,
   8.217 -   Metis_Thm.axiom (Metis_LiteralSet.fromList
   8.218 -                        (map m_arity_cls (concl_lits :: prem_lits))));
   8.219 -
   8.220 -(* CLASSREL CLAUSE *)
   8.221 -fun m_class_rel_cls (subclass, _) (superclass, _) =
   8.222 -  [metis_lit false subclass [Metis_Term.Var "T"],
   8.223 -   metis_lit true superclass [Metis_Term.Var "T"]]
   8.224 -fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) =
   8.225 -  (TrueI, m_class_rel_cls subclass superclass
   8.226 -          |> Metis_LiteralSet.fromList |> Metis_Thm.axiom)
   8.227 -
   8.228 -fun type_ext thy tms =
   8.229 -  let
   8.230 -    val subs = tfree_classes_of_terms tms
   8.231 -    val supers = tvar_classes_of_terms tms
   8.232 -    val tycons = type_constrs_of_terms thy tms
   8.233 -    val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   8.234 -    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   8.235 -  in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
   8.236 -
   8.237  val proxy_defs = map (fst o snd o snd) proxy_table
   8.238  val prepare_helper =
   8.239    Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
   8.240 @@ -346,92 +153,39 @@
   8.241    | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
   8.242  
   8.243  (* Function to generate metis clauses, including comb and type clauses *)
   8.244 -fun prepare_metis_problem ctxt (mode as Type_Sys type_sys) conj_clauses
   8.245 -                          fact_clauses =
   8.246 -    let
   8.247 -      val type_sys = type_sys_from_string type_sys
   8.248 -      val explicit_apply = NONE
   8.249 -      val clauses =
   8.250 -        conj_clauses @ fact_clauses
   8.251 -        |> (if polymorphism_of_type_sys type_sys = Polymorphic then
   8.252 -              I
   8.253 -            else
   8.254 -              map (pair 0)
   8.255 -              #> rpair ctxt
   8.256 -              #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
   8.257 -              #> fst #> maps (map (zero_var_indexes o snd)))
   8.258 -      val (old_skolems, props) =
   8.259 -        fold_rev (fn clause => fn (old_skolems, props) =>
   8.260 -                     clause |> prop_of |> Logic.strip_imp_concl
   8.261 -                            |> conceal_old_skolem_terms (length clauses)
   8.262 -                                                        old_skolems
   8.263 -                            ||> (fn prop => prop :: props))
   8.264 -             clauses ([], [])
   8.265 +fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
   8.266 +  let
   8.267 +    val type_sys = type_sys_from_string type_sys
   8.268 +    val explicit_apply = NONE
   8.269 +    val clauses =
   8.270 +      conj_clauses @ fact_clauses
   8.271 +      |> (if polymorphism_of_type_sys type_sys = Polymorphic then
   8.272 +            I
   8.273 +          else
   8.274 +            map (pair 0)
   8.275 +            #> rpair ctxt
   8.276 +            #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
   8.277 +            #> fst #> maps (map (zero_var_indexes o snd)))
   8.278 +    val (old_skolems, props) =
   8.279 +      fold_rev (fn clause => fn (old_skolems, props) =>
   8.280 +                   clause |> prop_of |> Logic.strip_imp_concl
   8.281 +                          |> conceal_old_skolem_terms (length clauses)
   8.282 +                                                      old_skolems
   8.283 +                          ||> (fn prop => prop :: props))
   8.284 +           clauses ([], [])
   8.285  (*
   8.286  val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
   8.287  *)
   8.288 -      val (atp_problem, _, _, _, _, _, sym_tab) =
   8.289 -        prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
   8.290 -                            false false props @{prop False} []
   8.291 +    val (atp_problem, _, _, _, _, _, sym_tab) =
   8.292 +      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
   8.293 +                          false false props @{prop False} []
   8.294  (*
   8.295  val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
   8.296  *)
   8.297 -      (* "rev" is for compatibility *)
   8.298 -      val axioms =
   8.299 -        atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
   8.300 -                    |> rev
   8.301 -    in
   8.302 -      (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
   8.303 -    end
   8.304 -  | prepare_metis_problem ctxt mode conj_clauses fact_clauses =
   8.305 -    let
   8.306 -      val thy = Proof_Context.theory_of ctxt
   8.307 -      (* The modes FO and FT are sticky. HO can be downgraded to FO. *)
   8.308 -      val mode =
   8.309 -        if mode = HO andalso
   8.310 -           forall (forall (is_quasi_fol_clause thy))
   8.311 -                  [conj_clauses, fact_clauses] then
   8.312 -          FO
   8.313 -        else
   8.314 -          mode
   8.315 -      fun add_thm is_conjecture (isa_ith, metis_ith)
   8.316 -                  {axioms, tfrees, old_skolems} : metis_problem =
   8.317 -        let
   8.318 -          val (mth, tfree_lits, old_skolems) =
   8.319 -            hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
   8.320 -                           metis_ith
   8.321 -        in
   8.322 -          {axioms = (mth, Isa_Raw isa_ith) :: axioms,
   8.323 -           tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
   8.324 -        end;
   8.325 -      fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} =
   8.326 -        {axioms = (mth, Isa_Raw ith) :: axioms, tfrees = tfrees,
   8.327 -         old_skolems = old_skolems}
   8.328 -      fun add_tfrees {axioms, tfrees, old_skolems} =
   8.329 -        {axioms = map (rpair (Isa_Raw TrueI) o metis_of_tfree)
   8.330 -                      (distinct (op =) tfrees) @ axioms,
   8.331 -         tfrees = tfrees, old_skolems = old_skolems}
   8.332 -      val problem =
   8.333 -        {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
   8.334 -        |> fold (add_thm true o `Meson.make_meta_clause) conj_clauses
   8.335 -        |> add_tfrees
   8.336 -        |> fold (add_thm false o `Meson.make_meta_clause) fact_clauses
   8.337 -      val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem)
   8.338 -      fun is_used c =
   8.339 -        exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
   8.340 -      val problem =
   8.341 -        if mode = FO then
   8.342 -          problem
   8.343 -        else
   8.344 -          let
   8.345 -            val helper_ths =
   8.346 -              helper_table
   8.347 -              |> filter (is_used o prefix const_prefix o fst o fst)
   8.348 -              |> maps (fn ((_, needs_full_types), thms) =>
   8.349 -                          if needs_full_types andalso mode <> FT then []
   8.350 -                          else map (`prepare_helper) thms)
   8.351 -          in problem |> fold (add_thm false) helper_ths end
   8.352 -      val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses))
   8.353 -    in (mode, Symtab.empty, fold add_type_thm type_ths problem) end
   8.354 +    (* "rev" is for compatibility *)
   8.355 +    val axioms =
   8.356 +      atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
   8.357 +                  |> rev
   8.358 +  in (sym_tab, axioms, old_skolems) end
   8.359  
   8.360  end;
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:36 2011 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:56:06 2011 +0200
     9.3 @@ -417,8 +417,8 @@
     9.4    in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
     9.5  
     9.6  fun tac_for_reconstructor Metis =
     9.7 -    Metis_Tactics.new_metis_tac [Metis_Tactics.default_unsound_type_sys]
     9.8 -  | tac_for_reconstructor MetisFT = Metis_Tactics.new_metisFT_tac
     9.9 +    Metis_Tactics.metis_tac [Metis_Tactics.default_unsound_type_sys]
    9.10 +  | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
    9.11    | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
    9.12  
    9.13  fun timed_reconstructor reconstructor debug timeout ths =
    10.1 --- a/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:36:36 2011 +0200
    10.2 +++ b/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:56:06 2011 +0200
    10.3 @@ -52,7 +52,7 @@
    10.4         THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
    10.5     ORELSE
    10.6     SOLVE_TIMEOUT (max_secs div 10) "metis"
    10.7 -       (ALLGOALS (Metis_Tactics.new_metis_tac [] ctxt []))
    10.8 +       (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
    10.9     ORELSE
   10.10     SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
   10.11     ORELSE
    11.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Mon Jun 06 20:36:36 2011 +0200
    11.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon Jun 06 20:56:06 2011 +0200
    11.3 @@ -70,7 +70,7 @@
    11.4    in
    11.5      case run_atp false timeout i i ctxt th atp of
    11.6        SOME facts =>
    11.7 -      Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    11.8 +      Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    11.9      | NONE => Seq.empty
   11.10    end
   11.11